src/Doc/JEdit/JEdit.thy
 changeset 69597 ff784d5a5bfb parent 69343 395c4fb15ea2 child 69854 cc0b3e177b49
equal inserted replaced
69596:c8a2755bf220 69597:ff784d5a5bfb
   162 text \<open>
   162 text \<open>
   163   Both jEdit and Isabelle have distinctive management of persistent options.
   163   Both jEdit and Isabelle have distinctive management of persistent options.
   164
   164
   165   Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ Global
   165   Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ Global
   166   Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip the
   166   Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip the
   167   two within the central options dialog. Changes are stored in @{path
   167   two within the central options dialog. Changes are stored in \<^path>\<open>$JEDIT_SETTINGS/properties\<close> and \<^path>\<open>$JEDIT_SETTINGS/keymaps\<close>.
   168   "$JEDIT_SETTINGS/properties"} and @{path "$JEDIT_SETTINGS/keymaps"}.

   169
   168
   170   Isabelle system options are managed by Isabelle/Scala and changes are stored
   169   Isabelle system options are managed by Isabelle/Scala and changes are stored
   171   in @{path "$ISABELLE_HOME_USER/etc/preferences"}, independently of  170 in \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close>, independently of
   172   other jEdit properties. See also @{cite "isabelle-system"}, especially the
   171   other jEdit properties. See also @{cite "isabelle-system"}, especially the
   173   coverage of sessions and command-line tools like @{tool build} or @{tool
   172   coverage of sessions and command-line tools like @{tool build} or @{tool
   174   options}.
   173   options}.
   175
   174
   176   Those Isabelle options that are declared as \<^verbatim>\<open>public\<close> are configurable in
   175   Those Isabelle options that are declared as \<^verbatim>\<open>public\<close> are configurable in
   188   The jEdit action @{action_def isabelle.options} opens the options dialog for
   187   The jEdit action @{action_def isabelle.options} opens the options dialog for
   189   the Isabelle plugin; it can be mapped to editor GUI elements as usual.
   188   the Isabelle plugin; it can be mapped to editor GUI elements as usual.
   190
   189
   191   \<^medskip>
   190   \<^medskip>
   192   Options are usually loaded on startup and saved on shutdown of
   191   Options are usually loaded on startup and saved on shutdown of
   193   Isabelle/jEdit. Editing the generated @{path "$JEDIT_SETTINGS/properties"}  192 Isabelle/jEdit. Editing the generated \<^path>\<open>$JEDIT_SETTINGS/properties\<close>
   194   or @{path "$ISABELLE_HOME_USER/etc/preferences"} manually while the  193 or \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> manually while the
   195   application is running may cause surprise due to lost updates!
   194   application is running may cause surprise due to lost updates!
   196 \<close>
   195 \<close>
   197
   196
   198
   197
   199 subsection \<open>Keymaps\<close>
   198 subsection \<open>Keymaps\<close>
   485   grouped according to some simple rules, e.g.\ as plain \<^verbatim>\<open>a\<close>'' or symbolic
   484   grouped according to some simple rules, e.g.\ as plain \<^verbatim>\<open>a\<close>'' or symbolic
   486   \<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of symbols is rendered
   485   \<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of symbols is rendered
   487   physically via Unicode glyphs, in order to show \<^verbatim>\<open>\<alpha>\<close>'' as \<open>\<alpha>\<close>'', for
   486   physically via Unicode glyphs, in order to show \<^verbatim>\<open>\<alpha>\<close>'' as \<open>\<alpha>\<close>'', for
   488   example. This symbol interpretation is specified by the Isabelle system
   487   example. This symbol interpretation is specified by the Isabelle system
   489   distribution in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the  488 distribution in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the
   490   user in @{path "$ISABELLE_HOME_USER/etc/symbols"}.  489 user in \<^path>\<open>$ISABELLE_HOME_USER/etc/symbols\<close>.
   491
   490
   492   The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
   491   The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
   493   standard interpretation of finitely many symbols from the infinite
   492   standard interpretation of finitely many symbols from the infinite
   494   collection. Uninterpreted symbols are displayed literally, e.g.\
   493   collection. Uninterpreted symbols are displayed literally, e.g.\
   495   \<^verbatim>\<open>\<foobar>\<close>''. Overlap of Unicode characters used in symbol
   494   \<^verbatim>\<open>\<foobar>\<close>''. Overlap of Unicode characters used in symbol
  1149 text \<open>
  1148 text \<open>
  1150   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Theorems\<close> mode retrieves facts from the theory
  1149   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Theorems\<close> mode retrieves facts from the theory
  1151   or proof context matching all of given criteria in the \<^emph>\<open>Find\<close> text field. A
  1150   or proof context matching all of given criteria in the \<^emph>\<open>Find\<close> text field. A
  1152   single criterion has the following syntax:
  1151   single criterion has the following syntax:
  1153
  1152
  1154   @{rail \<open>
  1153   \<^rail>\<open>
  1155     ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
  1154     ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
  1156       'solves' | 'simp' ':' @{syntax term} | @{syntax term})
  1155       'solves' | 'simp' ':' @{syntax term} | @{syntax term})
  1157   \<close>}
  1156   \<close>
  1158
  1157
  1159   See also the Isar command @{command_ref find_theorems} in @{cite
  1158   See also the Isar command @{command_ref find_theorems} in @{cite
  1160   "isabelle-isar-ref"}.
  1159   "isabelle-isar-ref"}.
  1161 \<close>
  1160 \<close>
  1162
  1161
  1166 text \<open>
  1165 text \<open>
  1167   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Constants\<close> mode prints all constants whose type
  1166   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Constants\<close> mode prints all constants whose type
  1168   meets all of the given criteria in the \<^emph>\<open>Find\<close> text field. A single
  1167   meets all of the given criteria in the \<^emph>\<open>Find\<close> text field. A single
  1169   criterion has the following syntax:
  1168   criterion has the following syntax:
  1170
  1169
  1171   @{rail \<open>
  1170   \<^rail>\<open>
  1172     ('-'?)
  1171     ('-'?)
  1173       ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
  1172       ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
  1174   \<close>}
  1173   \<close>
  1175
  1174
  1176   See also the Isar command @{command_ref find_consts} in @{cite
  1175   See also the Isar command @{command_ref find_consts} in @{cite
  1177   "isabelle-isar-ref"}.
  1176   "isabelle-isar-ref"}.
  1178 \<close>
  1177 \<close>
  1179
  1178
  1357
  1356
  1358 subsubsection \<open>Isabelle symbols\<close>
  1357 subsubsection \<open>Isabelle symbols\<close>
  1359
  1358
  1360 text \<open>
  1359 text \<open>
  1361   The completion tables for Isabelle symbols (\secref{sec:symbols}) are
  1360   The completion tables for Isabelle symbols (\secref{sec:symbols}) are
  1362   determined statically from \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and @{path  1361 determined statically from \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and \<^path>\<open>$ISABELLE_HOME_USER/etc/symbols\<close> for each symbol specification as follows:  1363 "$ISABELLE_HOME_USER/etc/symbols"} for each symbol specification as follows:

  1364
  1362
  1365   \<^medskip>
  1363   \<^medskip>
  1366   \begin{tabular}{ll}
  1364   \begin{tabular}{ll}
  1367   \<^bold>\<open>completion entry\<close> & \<^bold>\<open>example\<close> \\\hline
  1365   \<^bold>\<open>completion entry\<close> & \<^bold>\<open>example\<close> \\\hline
  1368   literal symbol & \<^verbatim>\<open>\<forall>\<close> \\
  1366   literal symbol & \<^verbatim>\<open>\<forall>\<close> \\
  1669
  1667
  1670   \<^item> @{system_option_def spell_checker_dictionary} determines the current
  1668   \<^item> @{system_option_def spell_checker_dictionary} determines the current
  1671   dictionary, taken from the colon-separated list in the settings variable
  1669   dictionary, taken from the colon-separated list in the settings variable
  1672   @{setting_def JORTHO_DICTIONARIES}. There are jEdit actions to specify local
  1670   @{setting_def JORTHO_DICTIONARIES}. There are jEdit actions to specify local
  1673   updates to a dictionary, by including or excluding words. The result of
  1671   updates to a dictionary, by including or excluding words. The result of
  1674   permanent dictionary updates is stored in the directory @{path
  1672   permanent dictionary updates is stored in the directory \<^path>\<open>$ISABELLE_HOME_USER/dictionaries\<close>, in a separate file for each dictionary.  1675 "$ISABELLE_HOME_USER/dictionaries"}, in a separate file for each dictionary.

  1676
  1673
  1677   \<^item> @{system_option_def spell_checker_include} specifies a comma-separated
  1674   \<^item> @{system_option_def spell_checker_include} specifies a comma-separated
  1678   list of markup elements that delimit words in the source that is subject to
  1675   list of markup elements that delimit words in the source that is subject to
  1679   spell-checking, including various forms of comments.
  1676   spell-checking, including various forms of comments.
  1680
  1677
  2006   usual support for antiquotations (like @{command ML}, @{command ML_file}).
  2003   usual support for antiquotations (like @{command ML}, @{command ML_file}).
  2007   Alternatively, strict Standard ML may be enforced via the \<^emph>\<open>SML\<close> checkbox
  2004   Alternatively, strict Standard ML may be enforced via the \<^emph>\<open>SML\<close> checkbox
  2008   (like @{command SML_file}).
  2005   (like @{command SML_file}).
  2009
  2006
  2010   The context for Isabelle/ML is optional, it may evaluate to a value of type
  2007   The context for Isabelle/ML is optional, it may evaluate to a value of type
  2011   @{ML_type theory}, @{ML_type Proof.context}, or @{ML_type Context.generic}.
  2008   \<^ML_type>\<open>theory\<close>, \<^ML_type>\<open>Proof.context\<close>, or \<^ML_type>\<open>Context.generic\<close>.
  2012   Thus the given ML expression (with its antiquotations) may be subject to the
  2009   Thus the given ML expression (with its antiquotations) may be subject to the
  2013   intended dynamic run-time context, instead of the static compile-time
  2010   intended dynamic run-time context, instead of the static compile-time
  2014   context.
  2011   context.
  2015
  2012
  2016   \<^medskip>
  2013   \<^medskip>
  2086   Parallel execution may add to the confusion. Peeking at physical process I/O
  2083   Parallel execution may add to the confusion. Peeking at physical process I/O
  2087   is only the last resort to diagnose problems with tools that are not PIDE
  2084   is only the last resort to diagnose problems with tools that are not PIDE
  2088   compliant.
  2085   compliant.
  2089
  2086
  2090   Under normal circumstances, prover output always works via managed message
  2087   Under normal circumstances, prover output always works via managed message
  2091   channels (corresponding to @{ML writeln}, @{ML warning}, @{ML
  2088   channels (corresponding to \<^ML>\<open>writeln\<close>, \<^ML>\<open>warning\<close>, \<^ML>\<open>Output.error_message\<close> in Isabelle/ML), which are displayed by regular means
  2092   Output.error_message} in Isabelle/ML), which are displayed by regular means

  2093   within the document model (\secref{sec:output}). Unhandled Isabelle/ML
  2089   within the document model (\secref{sec:output}). Unhandled Isabelle/ML
  2094   exceptions are printed by the system via @{ML Output.error_message}.
  2090   exceptions are printed by the system via \<^ML>\<open>Output.error_message\<close>.
  2095
  2091
  2096   \<^item> \<^emph>\<open>Syslog\<close> shows system messages that might be relevant to diagnose
  2092   \<^item> \<^emph>\<open>Syslog\<close> shows system messages that might be relevant to diagnose
  2097   problems with the startup or shutdown phase of the prover process; this also
  2093   problems with the startup or shutdown phase of the prover process; this also
  2098   includes raw output on \<^verbatim>\<open>stderr\<close>. Isabelle/ML also provides an explicit @{ML
  2094   includes raw output on \<^verbatim>\<open>stderr\<close>. Isabelle/ML also provides an explicit \<^ML>\<open>Output.system_message\<close> operation, which is occasionally useful for
  2099   Output.system_message} operation, which is occasionally useful for

  2100   diagnostic purposes within the system infrastructure itself.
  2095   diagnostic purposes within the system infrastructure itself.
  2101
  2096
  2102   A limited amount of syslog messages are buffered, independently of the
  2097   A limited amount of syslog messages are buffered, independently of the
  2103   docking state of the \<^emph>\<open>Syslog\<close> panel. This allows to diagnose serious
  2098   docking state of the \<^emph>\<open>Syslog\<close> panel. This allows to diagnose serious
  2104   problems with Isabelle/PIDE process management, outside of the actual
  2099   problems with Isabelle/PIDE process management, outside of the actual