| products/sources/formale Sprachen/Isabelle/Tools/jEdit/dist/doc/users-guide/settings-directory.html |
 |
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<title>The jEdit Settings Directory</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="customizing.html" title="Chapter 7. Customizing jEdit"><link rel="prev" href="global-opts.html" title="The Global Options Dialog Box"><link rel="next" href="using-macros.html" title="Chapter 8. Using Macros"></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 jEdit Settings Directory</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="global-opts.html">Prev</a> </td><th width="60%" align="center">Chapter 7. Customizing jEdit</th><td width="20%" align="right"> <a accesskey="n" href="using-macros.html">Next</a></td></tr></table><hr></div><div class="section"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a name="settings-directory"></a>The jEdit Settings Directory</h2></div></div></div><p>jEdit stores settings, keymaps, macros, and plugins as files inside the
<em class="firstterm">settings directory</em>. In most cases, editing these
files by hand is not necessary, since graphical tools and editor
commands can do the job. However, being familiar with the structure of
the settings directory still comes in handy in certain situations, for
example when you want to copy jEdit settings between computers.</p><p>The location of the settings directory is system-specific
<a href="#ftn.d0e6058" class="footnote" name="d0e6058"><sup class="footnote">[1]</sup></a>.
It is printed to the activity log
(<span class="guimenu"><strong>Utilities</strong></span>><span class="guisubmenu"><strong>Troubleshooting</strong></span>><span class="guimenuitem"><strong>Activity
Log</strong></span>). For example:</p><pre class="screen">[message] jEdit: Settings directory is /home/slava/.jedit</pre><p>Another way to find the location of your settings directory is to
use the "Utilities" menu, then the "Settings Directory" menu item. The
first item in the pullout menu is the location of your settings directory.
</p><p>From Console or the File System Browser, you can use an environment
variable, <code class="literal">$JEDIT_SETTINGS</code>, to refer to that location.
</p><p>Specifying the <strong class="userinput"><code>-settings</code></strong> switch on the
command line instructs jEdit to store settings in a directory other than
the default. For example, the following command will instruct jEdit to
store all settings in the <code class="filename">jedit</code> subdirectory of the
<code class="filename">C:</code> drive:</p><pre class="screen"><code class="prompt">C:\jedit></code> <strong class="userinput"><code>jedit -settings=C:\jedit</code></strong></pre><p>The <strong class="userinput"><code>-nosettings</code></strong> switch will force jEdit to
not look for or create a settings directory; default settings will be
used instead.</p><p>jEdit creates the following files and directories inside the
settings directory; plugins may add more:</p><div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; "><li class="listitem"><p><code class="filename">abbrevs</code> - a plain text file which
stores all defined abbreviations. See <a class="xref" href="abbrevs.html" title="Abbreviations">the section called “Abbreviations”</a>.</p></li><li class="listitem"><p><code class="filename">activity.log</code> - a plain text file
which contains the full activity log. See <a class="xref" href="activity-log.html" title="Appendix B. The Activity Log">Appendix B, <i>The Activity Log</i></a>.</p></li><li class="listitem"><p><code class="filename">history</code> - a plain text file which
stores history lists, used by history text fields and the
<span class="guimenu"><strong>Edit</strong></span>><span class="guimenuitem"><strong>Paste
Previous</strong></span> command. See <a class="xref" href="text-transfer.html" title="Transferring Text">the section called “Transferring Text”</a> and <a class="xref" href="history.html" title="Appendix C. History Text Fields">Appendix C, <i>History Text Fields</i></a>.</p></li><li class="listitem"><p><code class="filename">jars</code> - this directory contains
plugins. See <a class="xref" href="using-plugins.html" title="Chapter 9. Installing and Using Plugins">Chapter 9, <i>Installing and Using Plugins</i></a>.</p></li><li class="listitem"><p><code class="filename">jars-cache</code> - this directory contains
plugin cache files which decrease the time to start jEdit. They
are automatically updated when plugins are installed or
updated.</p></li><li class="listitem"><p><code class="filename">keymaps</code> - this directory
contains collections of named keyboard shortcuts
which can be defined from the Shortcuts Option Pane (see <a class="xref" href="global-opts.html#shortcuts-pane" title="The Shortcuts Pane">the section called “The Shortcuts Pane”</a>). </p></li><li class="listitem"><p><code class="filename">killring.xml</code> - stores recently
deleted text. See <a class="xref" href="text-transfer.html" title="Transferring Text">the section called “Transferring Text”</a>.</p></li><li class="listitem"><p><code class="filename">macros</code> - this directory contains
macros. See <a class="xref" href="using-macros.html" title="Chapter 8. Using Macros">Chapter 8, <i>Using Macros</i></a>.</p></li><li class="listitem"><p><code class="filename">modes</code> - this directory contains
custom edit modes. See <a class="xref" href="writing-modes-part.html" title="Part II. Writing Edit Modes">Part II, “Writing Edit Modes”</a>.</p></li><li class="listitem"><p><code class="filename">perspective.xml</code> - an XML file that
stores the list of open buffers and views used to maintain
editor state between sessions.</p></li><li class="listitem"><p><code class="filename">PluginManager.download</code> - this
directory is usually empty. It only contains files while the
plugin manager is downloading a plugin. For information about
the plugin manager, see <a class="xref" href="using-plugins.html" title="Chapter 9. Installing and Using Plugins">Chapter 9, <i>Installing and Using Plugins</i></a>.</p></li><li class="listitem"><p>
<code class="filename">pluginMgr-Cached.xml.gz</code> -
this contains a cached copy of the last XML plugin list downloaded from plugin central. If you delete this file, a new one will be created next time you try to install a plugin via Plugin Manager. </p></li><li class="listitem"><p><code class="filename">printspec</code> - a binary file that stores
printing settings.</p></li><li class="listitem"><p><code class="filename">properties</code> - a plain text file that
stores the majority of jEdit's and its plugins settings. For
more information see <a class="xref" href="settings-directory.html#propertiesfile" title="The jEdit properties file">the section called “The jEdit properties file”</a>.</p></li><li class="listitem"><p><code class="filename">recent.xml</code> - an XML file which stores
the list of recently opened files. jEdit remembers the caret
position and character encoding of each recent file, and
automatically restores those values when one of the files is
opened.</p></li><li class="listitem"><p><code class="filename">registers.xml</code> - an XML file that
stores register contents. See <a class="xref" href="text-transfer.html#registers" title="General Register Commands">the section called “General Register Commands”</a> for
more information about registers.</p></li><li class="listitem"><p><code class="filename">server</code> - a plain text file that only
exists while jEdit is running. The edit server's port number and
authorization key is stored here. See <a class="xref" href="starting.html" title="Chapter 2. Starting jEdit">Chapter 2, <i>Starting jEdit</i></a>.</p></li><li class="listitem"><p><code class="filename">settings-backup</code> - this directory
contains numbered backups of all automatically-written settings
files.</p></li><li class="listitem"><p><code class="filename">startup</code> - This directory
contains startup scripts in beanshell or other plugin-supported scripting
languages. They are run at the time jEdit starts, after the <code class="filename">startup</code> scripts in the jEdit install directory have been run. See <a class="xref" href="startup-scripts.html" title="Startup Scripts">the section called “Startup Scripts”</a></p></li></ul></div><div class="section"><div class="titlepage"><div><div><h3 class="title"><a name="propertiesfile"></a>The jEdit properties file</h3></div></div></div><p>The jEdit <code class="literal">properties</code> file uses the Java
properties syntax to store key/value pairs. All of the values are
stored as strings, but are interpreted as other types (such as
integer or boolean) by plugins at runtime.</p><p>Do not edit this file while jEdit is running. If you do, it
is possible that your changes (either your edits, or jEdit settings
changes) may get lost. </p></div><div class="section"><div class="titlepage"><div><div><h3 class="title"><a name="sitepropertiesfiles"></a>Site Properties</h3></div></div></div><p>
You may also put properties files in the <code class="filename">properties</code> directory under
the jEdit home directory (NOT the jedit settings directory). You
can locate the jEdit home directory by going to the Utilities menu
directory, then the <span class="guimenuitem"><strong>jEdit Home Directory</strong></span> menu item, and the first
item in the pullout menu will be the location of the jEdit home
directory. This is intended for site-wide settings. This lets you keep
custom user properties separate from the jEdit site-wide properties, so they are easier to find, edit, and move between machines. Note that your
custom properties files must have ".props" as the file name extension.
</p><p>
Prior to jEdit 5.0, this was also where site-wide keyboard shortcuts were placed, but now you can define custom sets of shortcuts as keymap files. These files can be cloned and edited from the Shortcuts Option Pane, or edited by hand. To place them in a system-wide location, copy them into the <code class="filename">keymaps</code> folder under the jedit home directory.
</p><p>
Site properties files are read in alphabetically by file name. This means
that if you have a property with the same name in more than one file,
the value for that property will be the value found in the last file
that was read.
</p><p>
You can edit these files inside jEdit - changes made to these files will not be re-read until the next time jEdit is started.
</p></div><div class="footnotes"><br><hr style="width:100; text-align:left;margin-left: 0"><div id="ftn.d0e6058" class="footnote"><p><a href="#d0e6058" class="para"><sup class="para">[1] </sup></a> On Linux, it is <code class="literal">~/.jedit</code>.
On Windows, you will find it in <code class="literal">%APPDATA%\jEdit</code>.
On the Mac, it is <code class="literal">~/Library/jEdit</code>.
</p></div></div></div><div class="navfooter"><hr><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="global-opts.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="customizing.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="using-macros.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">The Global Options Dialog Box </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 8. Using Macros</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.
|
