# HG changeset patch # User wenzelm # Date 1554921074 -7200 # Node ID f1c580ad34378769efed44883de063b8c9826376 # Parent 77f978dd8ffb00f66e702b3bd37eabfd8eccc27e tuned whitespace; diff -r 77f978dd8ffb -r f1c580ad3437 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Wed Apr 10 16:18:12 2019 +0200 +++ b/src/Doc/JEdit/JEdit.thy Wed Apr 10 20:31:14 2019 +0200 @@ -164,7 +164,8 @@ Regular jEdit options are accessible via the dialogs \<^emph>\Utilities~/ Global Options\ or \<^emph>\Plugins~/ Plugin Options\, with a second chance to flip the - two within the central options dialog. Changes are stored in \<^path>\$JEDIT_SETTINGS/properties\ and \<^path>\$JEDIT_SETTINGS/keymaps\. + two within the central options dialog. Changes are stored in + \<^path>\$JEDIT_SETTINGS/properties\ and \<^path>\$JEDIT_SETTINGS/keymaps\. Isabelle system options are managed by Isabelle/Scala and changes are stored in \<^path>\$ISABELLE_HOME_USER/etc/preferences\, independently of @@ -1360,7 +1361,9 @@ text \ The completion tables for Isabelle symbols (\secref{sec:symbols}) are - determined statically from \<^file>\$ISABELLE_HOME/etc/symbols\ and \<^path>\$ISABELLE_HOME_USER/etc/symbols\ for each symbol specification as follows: + determined statically from \<^file>\$ISABELLE_HOME/etc/symbols\ and + \<^path>\$ISABELLE_HOME_USER/etc/symbols\ for each symbol specification as + follows: \<^medskip> \begin{tabular}{ll} @@ -1671,7 +1674,9 @@ dictionary, taken from the colon-separated list in the settings variable @{setting_def JORTHO_DICTIONARIES}. There are jEdit actions to specify local updates to a dictionary, by including or excluding words. The result of - permanent dictionary updates is stored in the directory \<^path>\$ISABELLE_HOME_USER/dictionaries\, in a separate file for each dictionary. + permanent dictionary updates is stored in the directory + \<^path>\$ISABELLE_HOME_USER/dictionaries\, in a separate file for each + dictionary. \<^item> @{system_option_def spell_checker_include} specifies a comma-separated list of markup elements that delimit words in the source that is subject to @@ -2087,13 +2092,15 @@ compliant. Under normal circumstances, prover output always works via managed message - channels (corresponding to \<^ML>\writeln\, \<^ML>\warning\, \<^ML>\Output.error_message\ in Isabelle/ML), which are displayed by regular means - within the document model (\secref{sec:output}). Unhandled Isabelle/ML + channels (corresponding to \<^ML>\writeln\, \<^ML>\warning\, + \<^ML>\Output.error_message\ in Isabelle/ML), which are displayed by regular + means within the document model (\secref{sec:output}). Unhandled Isabelle/ML exceptions are printed by the system via \<^ML>\Output.error_message\. \<^item> \<^emph>\Syslog\ shows system messages that might be relevant to diagnose problems with the startup or shutdown phase of the prover process; this also - includes raw output on \<^verbatim>\stderr\. Isabelle/ML also provides an explicit \<^ML>\Output.system_message\ operation, which is occasionally useful for + includes raw output on \<^verbatim>\stderr\. Isabelle/ML also provides an explicit + \<^ML>\Output.system_message\ operation, which is occasionally useful for diagnostic purposes within the system infrastructure itself. A limited amount of syslog messages are buffered, independently of the