misc tuning and updates for release;
authorwenzelm
Thu Sep 21 13:21:36 2017 +0200 (21 months ago)
changeset 6668301189e46dc55
parent 66682 c4cbe609f6a8
child 66684 ace3cf4e1fbd
misc tuning and updates for release;
src/Doc/JEdit/JEdit.thy
src/Tools/jEdit/lib/Tools/jedit
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Thu Sep 21 12:47:16 2017 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu Sep 21 13:21:36 2017 +0200
     1.3 @@ -26,9 +26,9 @@
     1.4      \<^descr>[Isabelle/Scala] is the system programming language of Isabelle. It
     1.5      extends the pure logical environment of Isabelle/ML towards the outer
     1.6      world of graphical user interfaces, text editors, IDE frameworks, web
     1.7 -    services etc. Special infrastructure allows to transfer algebraic
     1.8 -    datatypes and formatted text easily between ML and Scala, using
     1.9 -    asynchronous protocol commands.
    1.10 +    services, SSH servers, SQL databases etc. Special infrastructure allows to
    1.11 +    transfer algebraic datatypes and formatted text easily between ML and
    1.12 +    Scala, using asynchronous protocol commands.
    1.13  
    1.14      \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. It
    1.15      is built around a concept of parallel and asynchronous document
    1.16 @@ -79,14 +79,14 @@
    1.17  
    1.18    The options allow to specify a logic session name, but the same selector is
    1.19    also accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). After
    1.20 -  application startup, the selected logic session image is provided
    1.21 +  startup of the Isabelle plugin, the selected logic session image is provided
    1.22    automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is
    1.23 -  absent or outdated wrt.\ its sources, the build process updates it while the
    1.24 -  text editor is running. Prover IDE functionality is only activated after
    1.25 +  absent or outdated wrt.\ its sources, the build process updates it within
    1.26 +  the running text editor. Prover IDE functionality is fully activated after
    1.27    successful termination of the build process. A failure may require changing
    1.28 -  some options and restart the application. Changing the logic session, or the
    1.29 -  underlying ML system platform (32\,bit versus 64\,bit) requires a restart of
    1.30 -  the application to take effect.
    1.31 +  some options and restart of the Isabelle plugin or application. Changing the
    1.32 +  logic session, or the underlying ML system platform (32\,bit versus 64\,bit)
    1.33 +  requires a restart of the whole application to take effect.
    1.34  
    1.35    \<^medskip>
    1.36    The main job of the Prover IDE is to manage sources and their changes,
    1.37 @@ -122,7 +122,7 @@
    1.38    individual plugins.
    1.39  
    1.40    Most of the information about jEdit is relevant for Isabelle/jEdit as well,
    1.41 -  but one needs to keep in mind that defaults sometimes differ, and the
    1.42 +  but users need to keep in mind that defaults sometimes differ, and the
    1.43    official jEdit documentation does not know about the Isabelle plugin with
    1.44    its support for continuous checking of formal source text: jEdit is a plain
    1.45    text editor, but Isabelle/jEdit is a Prover IDE.
    1.46 @@ -144,16 +144,17 @@
    1.47    sense how it is meant to work, before loading too many other plugins.
    1.48  
    1.49    \<^medskip>
    1.50 -  The \<^emph>\<open>Isabelle\<close> plugin provides the main Prover IDE functionality of
    1.51 -  Isabelle/jEdit: it manages the prover session in the background. A few
    1.52 +  The \<^emph>\<open>Isabelle\<close> plugin is responsible for the main Prover IDE functionality
    1.53 +  of Isabelle/jEdit: it manages the prover session in the background. A few
    1.54    additional plugins are bundled with Isabelle/jEdit for convenience or out of
    1.55 -  necessity, notably \<^emph>\<open>Console\<close> with its Isabelle/Scala sub-plugin
    1.56 +  necessity, notably \<^emph>\<open>Console\<close> with its \<^emph>\<open>Scala\<close> sub-plugin
    1.57    (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific
    1.58    parsers for document tree structure (\secref{sec:sidekick}). The
    1.59    \<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the
    1.60    formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins
    1.61    (e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies
    1.62 -  of bundled plugins, but have no particular use in Isabelle/jEdit. \<close>
    1.63 +  of bundled plugins, but have no particular use in Isabelle/jEdit.
    1.64 +\<close>
    1.65  
    1.66  
    1.67  subsection \<open>Options \label{sec:options}\<close>
    1.68 @@ -174,11 +175,11 @@
    1.69  
    1.70    Those Isabelle options that are declared as \<^verbatim>\<open>public\<close> are configurable in
    1.71    Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover, there
    1.72 -  are various options for rendering of document content, which are
    1.73 -  configurable via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin
    1.74 -  Options~/ Isabelle\<close> in jEdit provides a view on a subset of Isabelle system
    1.75 -  options. Note that some of these options affect general parameters that are
    1.76 -  relevant outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
    1.77 +  are various options for rendering document content, which are configurable
    1.78 +  via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin Options~/
    1.79 +  Isabelle\<close> in jEdit provides a view on a subset of Isabelle system options.
    1.80 +  Note that some of these options affect general parameters that are relevant
    1.81 +  outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
    1.82    @{system_option parallel_proofs} for the Isabelle build tool @{cite
    1.83    "isabelle-system"}, but it is possible to use the settings variable
    1.84    @{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds
    1.85 @@ -189,10 +190,9 @@
    1.86  
    1.87    \<^medskip>
    1.88    Options are usually loaded on startup and saved on shutdown of
    1.89 -  Isabelle/jEdit. Editing the machine-generated @{path
    1.90 -  "$JEDIT_SETTINGS/properties"} or @{path
    1.91 -  "$ISABELLE_HOME_USER/etc/preferences"} manually while the application is
    1.92 -  running is likely to cause surprise due to lost update!
    1.93 +  Isabelle/jEdit. Editing the generated @{path "$JEDIT_SETTINGS/properties"}
    1.94 +  or @{path "$ISABELLE_HOME_USER/etc/preferences"} manually while the
    1.95 +  application is running may cause surprise due to lost updates!
    1.96  \<close>
    1.97  
    1.98  
    1.99 @@ -205,14 +205,12 @@
   1.100    first start of the editor; afterwards the keymap file takes precedence and
   1.101    is no longer affected by change of default properties.
   1.102  
   1.103 -  Users may change their keymap later, but need to keep its content @{path
   1.104 -  "$JEDIT_SETTINGS/keymaps"} in sync with \<^verbatim>\<open>shortcut\<close> properties in
   1.105 -  \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
   1.106 +  Users may change their keymap later, but this may lead to conflicts with
   1.107 +  \<^verbatim>\<open>shortcut\<close> properties in \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
   1.108  
   1.109 -  \<^medskip>
   1.110    The action @{action_def "isabelle.keymap-merge"} helps to resolve pending
   1.111    Isabelle keymap changes that are in conflict with the current jEdit keymap;
   1.112 -  non-conflicting changes are always applied implicitly. This action is
   1.113 +  while non-conflicting changes are applied implicitly. This action is
   1.114    automatically invoked on Isabelle/jEdit startup.
   1.115  \<close>
   1.116  
   1.117 @@ -232,11 +230,13 @@
   1.118    Options are:
   1.119      -D NAME=X    set JVM system property
   1.120      -J OPTION    add JVM runtime option
   1.121 +                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
   1.122      -R           open ROOT entry of logic session and use its parent
   1.123      -b           build only
   1.124      -d DIR       include session directory
   1.125      -f           fresh build
   1.126      -j OPTION    add jEdit runtime option
   1.127 +                 (default $JEDIT_OPTIONS)
   1.128      -l NAME      logic image name
   1.129      -m MODE      add print mode for output
   1.130      -n           no build of session image on startup
   1.131 @@ -248,8 +248,8 @@
   1.132  
   1.133    The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic image to be used
   1.134    for proof processing. Additional session root directories may be included
   1.135 -  via option \<^verbatim>\<open>-d\<close> to augment that name space of @{tool build} @{cite
   1.136 -  "isabelle-system"}.
   1.137 +  via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also @{cite
   1.138 +  "isabelle-system"}).
   1.139  
   1.140    By default, the specified image is checked and built on demand. The \<^verbatim>\<open>-s\<close>
   1.141    option determines where to store the result session image of @{tool build}.
   1.142 @@ -266,11 +266,10 @@
   1.143    do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
   1.144    Isabelle/jEdit), without requiring command-line invocation.
   1.145  
   1.146 -  The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options allow to pass additional low-level options to
   1.147 -  the JVM or jEdit, respectively. The defaults are provided by the Isabelle
   1.148 -  settings environment @{cite "isabelle-system"}, but note that these only
   1.149 -  work for the command-line tool described here, and not the regular
   1.150 -  application.
   1.151 +  The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options pass additional low-level options to the JVM or
   1.152 +  jEdit, respectively. The defaults are provided by the Isabelle settings
   1.153 +  environment @{cite "isabelle-system"}, but note that these only work for the
   1.154 +  command-line tool described here, and not the regular application.
   1.155  
   1.156    The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
   1.157    directly to the underlying \<^verbatim>\<open>java\<close> process.
   1.158 @@ -299,7 +298,7 @@
   1.159  
   1.160    The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
   1.161    different server name. The default server name is the official distribution
   1.162 -  name (e.g.\ \<^verbatim>\<open>Isabelle2016-1\<close>). Thus @{tool jedit_client} can connect to the
   1.163 +  name (e.g.\ \<^verbatim>\<open>Isabelle2017\<close>). Thus @{tool jedit_client} can connect to the
   1.164    Isabelle desktop application without further options.
   1.165  
   1.166    The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
   1.167 @@ -317,7 +316,7 @@
   1.168  subsection \<open>Look-and-feel \label{sec:look-and-feel}\<close>
   1.169  
   1.170  text \<open>
   1.171 -  jEdit is a Java/AWT/Swing application with some ambition to support
   1.172 +  jEdit is a Java/AWT/Swing application with the ambition to support
   1.173    ``native'' look-and-feel on all platforms, within the limits of what Oracle
   1.174    as Java provider and major operating system distributors allow (see also
   1.175    \secref{sec:problems}).
   1.176 @@ -327,9 +326,9 @@
   1.177  
   1.178      \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by default.
   1.179  
   1.180 -    The Linux-specific \<^emph>\<open>GTK+\<close> also works under the side-condition that the
   1.181 -    overall GTK theme and options are selected in a way that works with Java
   1.182 -    AWT/Swing. The JVM has no direct influence of GTK rendering.
   1.183 +    The Linux-specific \<^emph>\<open>GTK+\<close> often works as well, but the overall GTK theme
   1.184 +    and options need to be selected to suite Java/AWT/Swing. Note that Java
   1.185 +    Virtual Machine has no direct influence of GTK rendering.
   1.186  
   1.187      \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default.
   1.188  
   1.189 @@ -342,13 +341,13 @@
   1.190      \<^emph>\<open>MacOSX\<close> plugin enabled all the time on that platform.
   1.191  
   1.192    Users may experiment with different Swing look-and-feels, but need to keep
   1.193 -  in mind that this extra variance of GUI functionality is unlikely to work in
   1.194 -  arbitrary combinations. The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close>
   1.195 -  should always work on all platforms, although they are technically and
   1.196 -  stylistically outdated. The historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
   1.197 +  in mind that this extra variance of GUI functionality often causes problems.
   1.198 +  The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work on all
   1.199 +  platforms, although they are technically and stylistically outdated. The
   1.200 +  historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
   1.201  
   1.202 -  After changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close>,
   1.203 -  Isabelle/jEdit should be restarted to take full effect.
   1.204 +  Changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close> may update the
   1.205 +  GUI only partially: proper restart of Isabelle/jEdit is usually required.
   1.206  \<close>
   1.207  
   1.208  
   1.209 @@ -357,7 +356,7 @@
   1.210  text \<open>
   1.211    In distant past, displays with $1024 \times 768$ or $1280 \times 1024$
   1.212    pixels were considered ``high resolution'' and bitmap fonts with 12 or 14
   1.213 -  pixels as adequate for text rendering. In 2016, we routinely see much higher
   1.214 +  pixels as adequate for text rendering. In 2017, we routinely see much higher
   1.215    resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or ``Ultra HD'' /
   1.216    ``4K'' at $3840 \times 2160$.
   1.217  
   1.218 @@ -721,8 +720,8 @@
   1.219      @{system_option_def "jedit_indent_newline"} (enabled by default).
   1.220  
   1.221      Regular input (via keyboard or completion) indents the current line
   1.222 -    whenever an new keyword is emerging the start of the line. This depends on
   1.223 -    option @{system_option_def "jedit_indent_input"} (enabled by default).
   1.224 +    whenever an new keyword is emerging at the start of the line. This depends
   1.225 +    on option @{system_option_def "jedit_indent_input"} (enabled by default).
   1.226  
   1.227      \<^descr>[Semantic indentation] adds additional white space to unstructured proof
   1.228      scripts (\<^theory_text>\<open>apply\<close> etc.) via number of subgoals. This requires information
   1.229 @@ -821,7 +820,7 @@
   1.230      concrete syntax of the @{command_ref theory} command @{cite
   1.231      "isabelle-isar-ref"};
   1.232  
   1.233 -    \<^enum> via \<^bold>\<open>auxiliary files\<close> that are loaded into a theory by special \<^emph>\<open>load
   1.234 +    \<^enum> via \<^bold>\<open>auxiliary files\<close> that are included into a theory by \<^emph>\<open>load
   1.235      commands\<close>, notably @{command_ref ML_file} and @{command_ref SML_file}
   1.236      @{cite "isabelle-isar-ref"}.
   1.237  
   1.238 @@ -837,10 +836,7 @@
   1.239  text \<open>
   1.240    The \<^emph>\<open>Theories\<close> panel (see also \figref{fig:theories}) provides an overview
   1.241    of the status of continuous checking of theory nodes within the document
   1.242 -  model. Unlike batch sessions of @{tool build} @{cite "isabelle-system"},
   1.243 -  theory nodes are identified by full path names; this allows to work with
   1.244 -  multiple (disjoint) Isabelle sessions simultaneously within the same editor
   1.245 -  session.
   1.246 +  model.
   1.247  
   1.248    \begin{figure}[!htb]
   1.249    \begin{center}
   1.250 @@ -854,13 +850,13 @@
   1.251    Theory imports are resolved automatically by the PIDE document model: all
   1.252    required files are loaded and stored internally, without the need to open
   1.253    corresponding jEdit buffers. Opening or closing editor buffers later on has
   1.254 -  no impact on the formal document content: it only affects visibility.
   1.255 +  no direct impact on the formal document content: it only affects visibility.
   1.256  
   1.257 -  In contrast, auxiliary files (e.g.\ from \<^verbatim>\<open>ML_file\<close> commands) are \<^emph>\<open>not\<close>
   1.258 -  resolved within the editor by default, but the prover process takes care of
   1.259 -  that. This may be changed by enabling the system option @{system_option
   1.260 -  jedit_auto_resolve}: it ensures that all files are uniformly provided by the
   1.261 -  editor.
   1.262 +  In contrast, auxiliary files (e.g.\ from @{command ML_file} commands) are
   1.263 +  \<^emph>\<open>not\<close> resolved within the editor by default, but the prover process takes
   1.264 +  care of that. This may be changed by enabling the system option
   1.265 +  @{system_option jedit_auto_resolve}: it ensures that all files are uniformly
   1.266 +  provided by the editor.
   1.267  
   1.268    \<^medskip>
   1.269    The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective
   1.270 @@ -878,6 +874,10 @@
   1.271    visibility status (if continuous checking is enabled). Big theory libraries
   1.272    that are marked as required can have significant impact on performance!
   1.273  
   1.274 +  The \<^emph>\<open>Purge\<close> button restricts the document model to theories that are
   1.275 +  required for open editor buffers: inaccessible theories are removed and will
   1.276 +  be rechecked when opened or imported later.
   1.277 +
   1.278    \<^medskip>
   1.279    Formal markup of checked theory content is turned into GUI rendering, based
   1.280    on a standard repertoire known from mainstream IDEs for programming
   1.281 @@ -913,7 +913,9 @@
   1.282    edited conveniently in the Prover IDE on small machines with only 8\,GB of
   1.283    main memory. Using \<^verbatim>\<open>Pure\<close> as logic session image, the exploration may start
   1.284    at the top \<^file>\<open>$ISABELLE_HOME/src/HOL/Main.thy\<close> or the bottom
   1.285 -  \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example.
   1.286 +  \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example. It is also possible to
   1.287 +  explore the Isabelle/Pure bootstrap process (a virtual copy) by opening
   1.288 +  \<^file>\<open>$ISABELLE_HOME/src/Pure/ROOT.ML\<close> like a theory in the Prover IDE.
   1.289  
   1.290    Initially, before an auxiliary file is opened in the editor, the prover
   1.291    reads its content from the physical file-system. After the file is opened
   1.292 @@ -981,9 +983,11 @@
   1.293    The \<^emph>\<open>Theories\<close> panel provides another course-grained overview, but without
   1.294    direct correspondence to text positions. The coloured rectangles represent
   1.295    the amount of messages of a certain kind (warnings, errors, etc.) and the
   1.296 -  execution status of commands. A double-click on one of the theory entries
   1.297 -  with their status overview opens the corresponding text buffer, without
   1.298 -  moving the cursor to a specific point.
   1.299 +  execution status of commands. The border of each rectangle indicates the
   1.300 +  overall status of processing: a thick border means it is \<^emph>\<open>finished\<close> or
   1.301 +  \<^emph>\<open>failed\<close> (with color for errors). A double-click on one of the theory
   1.302 +  entries with their status overview opens the corresponding text buffer,
   1.303 +  without moving the cursor to a specific point.
   1.304  
   1.305    \<^medskip>
   1.306    The \<^emph>\<open>Output\<close> panel displays prover messages that correspond to a given
   1.307 @@ -1878,6 +1882,16 @@
   1.308  \<close>
   1.309  
   1.310  
   1.311 +section \<open>Document preview\<close>
   1.312 +
   1.313 +text \<open>
   1.314 +  The action @{action_def isabelle.preview} opens an HTML preview of the
   1.315 +  current theory document in the default web browser. The content is derived
   1.316 +  from the semantic markup produced by the prover, and thus depends on the
   1.317 +  status of formal processing.
   1.318 +\<close>
   1.319 +
   1.320 +
   1.321  chapter \<open>ML debugging within the Prover IDE\<close>
   1.322  
   1.323  text \<open>
   1.324 @@ -2065,12 +2079,6 @@
   1.325    \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from elsewhere, or disable
   1.326    continuous checking temporarily.
   1.327  
   1.328 -  \<^item> \<^bold>\<open>Problem:\<close> No direct support to remove document nodes from the collection
   1.329 -  of theories.
   1.330 -
   1.331 -  \<^bold>\<open>Workaround:\<close> Clear the buffer content of unused files and close \<^emph>\<open>without\<close>
   1.332 -  saving changes.
   1.333 -
   1.334    \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the
   1.335    editor font size depend on platform details and national keyboards.
   1.336  
   1.337 @@ -2096,15 +2104,6 @@
   1.338  
   1.339    \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font.
   1.340  
   1.341 -  \<^item> \<^bold>\<open>Problem:\<close> Mac OS X with Retina display has problems to determine the
   1.342 -  font metrics of \<^verbatim>\<open>IsabelleText\<close> accurately, notably in plain Swing text
   1.343 -  fields (e.g.\ in the \<^emph>\<open>Search and Replace\<close> dialog).
   1.344 -
   1.345 -  \<^bold>\<open>Workaround:\<close> Install \<^verbatim>\<open>IsabelleText\<close> and \<^verbatim>\<open>IsabelleTextBold\<close> on the system
   1.346 -  with \<^emph>\<open>Font Book\<close>, despite the warnings in \secref{sec:symbols} against
   1.347 -  that! The \<^verbatim>\<open>.ttf\<close> font files reside in some directory @{path
   1.348 -  "$ISABELLE_HOME/contrib/isabelle_fonts-XYZ"}.
   1.349 -
   1.350    \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
   1.351    event handling of Java/AWT/Swing.
   1.352  
   1.353 @@ -2136,7 +2135,7 @@
   1.354    \<^bold>\<open>Workaround:\<close> On a 64bit platform, ensure that the JVM runs in 64bit mode,
   1.355    but the Isabelle/ML process remains in 32bit mode! Do not switch Isabelle/ML
   1.356    into 64bit mode in the expectation to be ``more efficient'' --- this
   1.357 -  requires approx.\ 32\,GB to make sense.
   1.358 +  requires 16--32\,GB to make sense.
   1.359  
   1.360    For the JVM, always use the 64bit version. That is the default on all
   1.361    platforms, except for Windows: the standard download is for win32, but there
     2.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Thu Sep 21 12:47:16 2017 +0200
     2.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Sep 21 13:21:36 2017 +0200
     2.3 @@ -110,13 +110,14 @@
     2.4    echo
     2.5    echo "  Options are:"
     2.6    echo "    -D NAME=X    set JVM system property"
     2.7 -  echo "    -J OPTION    add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
     2.8 +  echo "    -J OPTION    add JVM runtime option"
     2.9 +  echo "                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
    2.10    echo "    -R           open ROOT entry of logic session and use its parent"
    2.11    echo "    -b           build only"
    2.12    echo "    -d DIR       include session directory"
    2.13    echo "    -f           fresh build"
    2.14    echo "    -j OPTION    add jEdit runtime option"
    2.15 -  echo "                 (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
    2.16 +  echo "                 (default $JEDIT_OPTIONS)"
    2.17    echo "    -l NAME      logic session name"
    2.18    echo "    -m MODE      add print mode for output"
    2.19    echo "    -n           no build of session image on startup"