| products/sources/formale sprachen/Isabelle/Tools/jEdit/dist/doc/users-guide/plugin-manager.html |
 |
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<title>The Plugin Manager</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="using-plugins.html" title="Chapter 9. Installing and Using Plugins"><link rel="next" href="installing-plugins.html" title="Installing and Updating Plugins"></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">The Plugin Manager</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="using-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="installing-plugins.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-manager"></a>The Plugin Manager</h2></div></div></div><p><span class="guimenu"><strong>Plugins</strong></span>><span class="guimenuitem"><strong>Plugin
Manager</strong></span> displays the plugin manager window. It consists of
three tabs: Manage, Update and Install. The Manage tab lists all
installed plugins; clicking on a plugin in the list will display
information about it.</p><p>To remove plugins, select them (multiple plugins can be selected
by holding down <code class="keycap">Control</code>) and click
<span class="guibutton"><strong>Remove</strong></span>. This will display a confirmation dialog
box first.</p><p>To view plugin documentation, select a plugin and click
<span class="guibutton"><strong>Help</strong></span>. Note that plugin documentation can also be
accessed by invoking <span class="guimenu"><strong>Help</strong></span>><span class="guimenuitem"><strong>jEdit
Help</strong></span>.</p><p> After you have tuned jEdit to your liking and want to install the
same set of plugins onto another host, or another user's profile, you
can export your currently installed plugin list as an xml file, known as
a <span class="bold"><strong>PluginSet</strong></span>. The
<span class="guibutton"><strong>Save</strong></span> rollover button allows you to save the list
of installed and loaded plugins to an XML file. See <a class="xref" href="plugin-sets.html" title="Plugin Sets">the section called “Plugin Sets”</a> for more information. </p><p><span class="guimenu"><strong>Plugins</strong></span>><span class="guimenuitem"><strong>Plugin
Options</strong></span> displays a dialog box for changing plugin
settings.</p></div><div class="navfooter"><hr><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="using-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="installing-plugins.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">Chapter 9. Installing and Using Plugins </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Installing and Updating Plugins</td></tr></table></div></body></html>
¤ Dauer der Verarbeitung: 0.16 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.
|
