--- a/src/Doc/JEdit/JEdit.thy Thu Aug 11 18:26:16 2016 +0200
+++ b/src/Doc/JEdit/JEdit.thy Thu Aug 11 18:26:44 2016 +0200
@@ -166,12 +166,12 @@
Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ Global
Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip the
- two within the central options dialog. Changes are stored in
- @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"} and
- @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}.
+ two within the central options dialog. Changes are stored in @{path
+ "$ISABELLE_HOME_USER/jedit/properties"} and @{path
+ "$ISABELLE_HOME_USER/jedit/keymaps"}.
Isabelle system options are managed by Isabelle/Scala and changes are stored
- in @{file_unchecked "$ISABELLE_HOME_USER/etc/preferences"}, independently of
+ in @{path "$ISABELLE_HOME_USER/etc/preferences"}, independently of
other jEdit properties. See also @{cite "isabelle-system"}, especially the
coverage of sessions and command-line tools like @{tool build} or @{tool
options}.
@@ -193,8 +193,8 @@
\<^medskip>
Options are usually loaded on startup and saved on shutdown of
- Isabelle/jEdit. Editing the machine-generated @{file_unchecked
- "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked
+ Isabelle/jEdit. Editing the machine-generated @{path
+ "$ISABELLE_HOME_USER/jedit/properties"} or @{path
"$ISABELLE_HOME_USER/etc/preferences"} manually while the application is
running is likely to cause surprise due to lost update!
\<close>
@@ -213,9 +213,8 @@
Isabelle/jEdit due to various fine-tuning of global defaults, with
additional keyboard shortcuts for Isabelle-specific functionality. Users may
change their keymap later, but need to copy some keyboard shortcuts manually
- (see also @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"} versus
- \<^verbatim>\<open>shortcut\<close> properties in @{file
- "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}).
+ (see also @{path "$ISABELLE_HOME_USER/jedit/keymaps"} versus \<^verbatim>\<open>shortcut\<close>
+ properties in @{file "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}).
\<close>
@@ -470,7 +469,7 @@
physically via Unicode glyphs, in order to show ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for
example. This symbol interpretation is specified by the Isabelle system
distribution in @{file "$ISABELLE_HOME/etc/symbols"} and may be augmented by
- the user in @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"}.
+ the user in @{path "$ISABELLE_HOME_USER/etc/symbols"}.
The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
standard interpretation of finitely many symbols from the infinite
@@ -660,9 +659,9 @@
platforms. Isabelle/ML on Windows uses Unix-style path notation, too, and
driver letter representation as in Cygwin (e.g.\ \<^verbatim>\<open>/cygdrive/c\<close>). Moreover,
environment variables from the Isabelle process may be used freely, e.g.\
- @{file "$ISABELLE_HOME/etc/symbols"} or @{file_unchecked
- "$POLYML_HOME/README"}. There are special shortcuts: @{file "~"} for @{file
- "$USER_HOME"} and @{file "~~"} for @{file "$ISABELLE_HOME"}.
+ @{file "$ISABELLE_HOME/etc/symbols"} or @{file "$POLYML_HOME/README"}. There
+ are special shortcuts: @{dir "~"} for @{dir "$USER_HOME"} and @{dir "~~"}
+ for @{dir "$ISABELLE_HOME"}.
\<^medskip>
Since jEdit happens to support environment variables within file
@@ -1242,7 +1241,7 @@
text \<open>
The completion tables for Isabelle symbols (\secref{sec:symbols}) are
determined statically from @{file "$ISABELLE_HOME/etc/symbols"} and
- @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"} for each symbol
+ @{path "$ISABELLE_HOME_USER/etc/symbols"} for each symbol
specification as follows:
\<^medskip>
@@ -1274,12 +1273,12 @@
\<^medskip>
Additional abbreviations may be specified in @{file
- "$ISABELLE_HOME/etc/abbrevs"} and @{file_unchecked
- "$ISABELLE_HOME_USER/etc/abbrevs"}. The file content follows general Isar
- outer syntax @{cite "isabelle-isar-ref"}. Abbreviations are specified as
+ "$ISABELLE_HOME/etc/abbrevs"} and @{path "$ISABELLE_HOME_USER/etc/abbrevs"}.
+ The file content follows general Isar outer syntax @{cite
+ "isabelle-isar-ref"}. Abbreviations are specified as
``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may consist of more
than just one symbol; otherwise the meaning is the same as a symbol
- specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{file_unchecked
+ specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{path
"etc/symbols"}.
\<close>
@@ -1544,7 +1543,7 @@
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 @{file_unchecked
+ 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_elements} specifies a comma-separated
@@ -2003,7 +2002,7 @@
\<^bold>\<open>Workaround:\<close> Install \<^verbatim>\<open>IsabelleText\<close> and \<^verbatim>\<open>IsabelleTextBold\<close> on the system
with \<^emph>\<open>Font Book\<close>, despite the warnings in \secref{sec:symbols} against
- that! The \<^verbatim>\<open>.ttf\<close> font files reside in some directory @{file_unchecked
+ that! The \<^verbatim>\<open>.ttf\<close> font files reside in some directory @{path
"$ISABELLE_HOME/contrib/isabelle_fonts-XYZ"}.
\<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key