| products/sources/formale Sprachen/Isabelle/Tools/jEdit/dist/doc/tips/tip31.html |
 |
<html><body>
Any scripts located in the <code>startup</code> subdirectory of the
jEdit home and user settings directories will be run on jEdit startup. Scripts can
be written in BeanShell or any scripting language for which the appropriate
plugin is installed (for example, Python scripting is provided by the
<b>JythonInterpreter</b> plugin).<p>
Methods
and variables defined in BeanShell scripts are available to all other uses of
BeanShell in jEdit. This is different from macros; methods and variables defined
in macros are lost after the macro finishes executing.
</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.
|
