| products/Sources/formale Sprachen/Isabelle/Tools/jEdit/dist/doc/users-guide/plugin-sets.html |
 |
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<title>Plugin Sets</title><meta name="generator" content="DocBook XSL Stylesheets V1.79.1"><link rel="home" href="index.html" title="jEdit 5.6 User's Guide"><link rel="up" href="using-plugins.html" title="Chapter 9. Installing and Using Plugins"><link rel="prev" href="installing-plugins.html" title="Installing and Updating Plugins"><link rel="next" href="shortcuts.html" title="Appendix A. Keyboard Shortcuts"></head><body bgcolor="white" text="black" link="#0000FF" vlink="#840084" alink="#0000FF"><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Plugin Sets</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="installing-plugins.html">Prev</a> </td><th width="60%" align="center">Chapter 9. Installing and Using Plugins</th><td width="20%" align="right"> <a accesskey="n" href="shortcuts.html">Next</a></td></tr></table><hr></div><div class="section"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a name="plugin-sets"></a>Plugin Sets</h2></div></div></div><p> A <span class="bold"><strong>PluginSet</strong></span> is a collection of
plugins, represented as an XML file. These XML files can be created from the
<span class="guibutton"><strong>save</strong></span> button of the Manage tab of the Plugin Manager.
Saving a PluginSet remembers all of the currently loaded plugins. </p><p> When a PluginSet has been saved, it becomes the "default pluginset",
which means that if you unload/uninstall plugins from that set and go back to the
Install tab, you should see them selected for download again. To clear this
setting, click on the <span class="guibutton"><strong>clear</strong></span> button in the
Install tab.
</p><p> It is posisble to Choose/Open a PluginSet from the Manage or the
Install tab. The behavior of choosing a PluginSet depends on which tab
you are on when you choose it. From the Manage tab, it unloads plugins that
are loaded but not in the list. From the Install tab, it selects plugins
from that list that are not loaded, marking them for download from Plugin
Central. </p><p> When choosing a PluginSet, the path can be given as a remote URL.
This helps teachers and sysadmins direct the students/slaves to a standard
set of plugins that are required for the course/job. </p></div><div class="navfooter"><hr><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="installing-plugins.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="using-plugins.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="shortcuts.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Installing and Updating Plugins </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Appendix A. Keyboard Shortcuts</td></tr></table></div></body></html>
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
