misc tuning;
authorwenzelm
Thu Nov 07 13:34:04 2013 +0100 (2013-11-07)
changeset 543722d61935eed4a
parent 54371 52ed202464a5
child 54373 232cf1e475da
misc tuning;
src/Doc/JEdit/JEdit.thy
src/Doc/antiquote_setup.ML
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Wed Nov 06 21:20:20 2013 +0100
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu Nov 07 13:34:04 2013 +0100
     1.3 @@ -37,8 +37,8 @@
     1.4    Isabelle. It extends the pure logical environment of Isabelle/ML
     1.5    towards the ``real world'' of graphical user interfaces, text
     1.6    editors, IDE frameworks, web services etc.  Special infrastructure
     1.7 -  allows to transfer algebraic datatype values and formatted text
     1.8 -  easily between ML and Scala, using asynchronous protocol commands.
     1.9 +  allows to transfer algebraic datatypes and formatted text easily
    1.10 +  between ML and Scala, using asynchronous protocol commands.
    1.11  
    1.12    \item [jEdit] is a sophisticated text editor implemented in
    1.13    Java.\footnote{\url{http://www.jedit.org}} It is easily extensible
    1.14 @@ -48,9 +48,9 @@
    1.15    \item [Isabelle/jEdit] is the main example application of the PIDE
    1.16    framework and the default user-interface for Isabelle. It targets
    1.17    both beginners and experts. Technically, Isabelle/jEdit combines a
    1.18 -  slightly modified version of the official jEdit code base with a
    1.19 -  special plugin for Isabelle, integrated as standalone application
    1.20 -  for the main operating system platforms: Linux, Windows, Mac OS X.
    1.21 +  slightly modified version of the jEdit code base with a special
    1.22 +  plugin for Isabelle, integrated as standalone application for the
    1.23 +  main operating system platforms: Linux, Windows, Mac OS X.
    1.24  
    1.25    \end{description}
    1.26  
    1.27 @@ -136,7 +136,7 @@
    1.28  
    1.29  text {* The \emph{Plugin Manager} of jEdit allows to augment editor
    1.30    functionality by JVM modules (jars) that are provided by the central
    1.31 -  plugin repository, which is accessible by various mirror sites.
    1.32 +  plugin repository, which is accessible via various mirror sites.
    1.33  
    1.34    Connecting to the plugin server infrastructure of the jEdit project
    1.35    allows to update bundled plugins or to add further functionality.
    1.36 @@ -162,30 +162,31 @@
    1.37  text {* Both jEdit and Isabelle have distinctive management of
    1.38    persistent options.
    1.39  
    1.40 -  Regular jEdit options are accessible via the dialogs for
    1.41 -  \emph{Global Options} and \emph{Plugin Options}.  Changed properties
    1.42 -  are stored eventually in @{verbatim
    1.43 -  "$ISABELLE_HOME_USER/jedit/properties"}.  In contrast, Isabelle
    1.44 -  system options are managed by Isabelle/Scala and changes stored in
    1.45 -  @{verbatim "$ISABELLE_HOME_USER/etc/preferences"}, independently of
    1.46 -  the jEdit properties.  See also \cite{isabelle-sys}, especially the
    1.47 -  coverage of sessions and command-line tools like @{tool build} or
    1.48 -  @{tool options}.
    1.49 +  Regular jEdit options are accessible via the dialog for
    1.50 +  \emph{Plugins / Plugin Options}, which is also accessible via
    1.51 +  \emph{Utilities / Global Options}.  Changed properties are stored in
    1.52 +  @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"}.  In
    1.53 +  contrast, Isabelle system options are managed by Isabelle/Scala and
    1.54 +  changed values stored in @{file_unchecked
    1.55 +  "$ISABELLE_HOME_USER/etc/preferences"}, independently of the jEdit
    1.56 +  properties.  See also \cite{isabelle-sys}, especially the coverage
    1.57 +  of sessions and command-line tools like @{tool build} or @{tool
    1.58 +  options}.
    1.59  
    1.60    Those Isabelle options that are declared as \textbf{public} are
    1.61    configurable in jEdit via \emph{Plugin Options / Isabelle /
    1.62    General}.  Moreover, there are various options for rendering of
    1.63    document content, which are configurable via \emph{Plugin Options /
    1.64    Isabelle / Rendering}.  Thus \emph{Plugin Options / Isabelle} in
    1.65 -  jEdit provides a view on certain Isabelle options.  Note that some
    1.66 -  of these options affect general parameters that are relevant outside
    1.67 -  Isabelle/jEdit as well, e.g.\ @{system_option threads} or
    1.68 -  @{system_option parallel_proofs} for the Isabelle build tool
    1.69 -  \cite{isabelle-sys}.
    1.70 +  jEdit provides a view on a subset of Isabelle system options.  Note
    1.71 +  that some of these options affect general parameters that are
    1.72 +  relevant outside Isabelle/jEdit as well, e.g.\ @{system_option
    1.73 +  threads} or @{system_option parallel_proofs} for the Isabelle build
    1.74 +  tool \cite{isabelle-sys}.
    1.75  
    1.76    \medskip All options are loaded on startup and saved on shutdown of
    1.77 -  Isabelle/jEdit.  Editing the machine-generated files @{verbatim
    1.78 -  "$ISABELLE_HOME_USER/jedit/properties"} or @{verbatim
    1.79 +  Isabelle/jEdit.  Editing the machine-generated @{file_unchecked
    1.80 +  "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked
    1.81    "$ISABELLE_HOME_USER/etc/preferences"} manually while the
    1.82    application is running is likely to cause surprise due to lost
    1.83    update!  *}
    1.84 @@ -202,8 +203,9 @@
    1.85  
    1.86    This is relevant for Isabelle/jEdit due to various fine-tuning of
    1.87    default properties, and additional keyboard shortcuts for Isabelle
    1.88 -  specific functionality. Users may change their keymap, but need to
    1.89 -  copy Isabelle-specific key bindings manually.  *}
    1.90 +  specific functionality. Users may change their keymap later, but
    1.91 +  need to copy Isabelle-specific key bindings manually (see also
    1.92 +  @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}).  *}
    1.93  
    1.94  
    1.95  subsection {* Look-and-feel *}
    1.96 @@ -219,17 +221,18 @@
    1.97    \begin{description}
    1.98  
    1.99    \item[Linux] The platform-independent \emph{Nimbus} is used by
   1.100 -  default, but the classic \emph{Metal} also works.  \emph{GTK+} works
   1.101 -  under the side-condition that the overall GTK theme is selected in a
   1.102 -  Swing-friendly way.\footnote{GTK support in Java/Swing was once
   1.103 -  marketed aggressively by Sun, but never quite finished, and is today
   1.104 -  (2013) lagging a bit behind further development of Swing and GTK.}
   1.105 +  default.
   1.106  
   1.107 -  \item[Windows] Regular \emph{Windows} is used by default, but
   1.108 -  platform-independent \emph{Nimbus} and \emph{Metal} also work.
   1.109 +  \emph{GTK+} works under the side-condition that the overall GTK
   1.110 +  theme is selected in a Swing-friendly way.\footnote{GTK support in
   1.111 +  Java/Swing was once marketed aggressively by Sun, but never quite
   1.112 +  finished, and is today (2013) lagging a bit behind further
   1.113 +  development of Swing and GTK.}
   1.114  
   1.115 -  \item[Mac OS X] Regular \emph{Mac OS X} is used by default, but
   1.116 -  platform-independent \emph{Nimbus} and \emph{Metal} also work.
   1.117 +  \item[Windows] Regular \emph{Windows} is used by default.
   1.118 +
   1.119 +  \item[Mac OS X] Regular \emph{Mac OS X} is used by default.
   1.120 +
   1.121    Moreover the bundled \emph{MacOSX} plugin provides various functions
   1.122    that are expected from applications on that particular platform:
   1.123    quit from menu or dock, preferences menu, drag-and-drop of text
   1.124 @@ -240,13 +243,18 @@
   1.125  
   1.126    Users may experiment with different look-and-feels, but need to keep
   1.127    in mind that this extra variance of GUI functionality is unlikely to
   1.128 -  work in arbitrary combinations.  The historic \emph{CDE/Motif} is
   1.129 -  better avoided.  After changing the look-and-feel in \emph{Global
   1.130 -  Options / Appearance}, it is advisable to restart Isabelle/jEdit in
   1.131 -  order to take full effect.  *}
   1.132 +  work in arbitrary combinations.  The platform-independent
   1.133 +  \emph{Nimbus} and \emph{Metal} should always work.  The historic
   1.134 +  \emph{CDE/Motif} is better avoided.
   1.135 +
   1.136 +  After changing the look-and-feel in \emph{Global Options /
   1.137 +  Appearance}, it is advisable to restart Isabelle/jEdit in order to
   1.138 +  take full effect.  *}
   1.139  
   1.140  
   1.141 -subsection {* File-system access *}
   1.142 +chapter {* Prover IDE functionality *}
   1.143 +
   1.144 +section {* File-system access *}
   1.145  
   1.146  text {* File specifications in jEdit follow various formats and
   1.147    conventions according to \emph{Virtual File Systems}, which may be
   1.148 @@ -271,8 +279,8 @@
   1.149    Isabelle process may be used freely, e.g.\ @{file
   1.150    "$ISABELLE_HOME/etc/symbols"} or @{file
   1.151    "$ISABELLE_JDK_HOME/README.html"}.  There are special shortcuts:
   1.152 -  @{verbatim "~"} for @{file "$USER_HOME"}, and @{verbatim "~~"} for
   1.153 -  @{file "$ISABELLE_HOME"}.
   1.154 +  @{file "~"} for @{file "$USER_HOME"} and @{file "~~"} for @{file
   1.155 +  "$ISABELLE_HOME"}.
   1.156  
   1.157    \medskip Since jEdit happens to support environment variables within
   1.158    file specifications as well, it is natural to use similar notation
   1.159 @@ -295,8 +303,6 @@
   1.160    notation.  *}
   1.161  
   1.162  
   1.163 -chapter {* Prover IDE functionality *}
   1.164 -
   1.165  section {* Text buffers and theories \label{sec:buffers-theories} *}
   1.166  
   1.167  text {* As regular text editor, jEdit maintains a collection of open
   1.168 @@ -321,8 +327,7 @@
   1.169    order to be included in the theory document model for further
   1.170    checking.  It is also possible to resolve dependencies
   1.171    automatically, depending on \emph{Plugin Options / Isabelle /
   1.172 -  General / Auto load} (Isabelle system option @{system_option
   1.173 -  jedit_auto_load}).
   1.174 +  General / Auto load}.
   1.175  
   1.176    \medskip The open text area views on theory buffers define the
   1.177    visible \emph{perspective} of Isabelle/jEdit.  This is taken as a
   1.178 @@ -330,7 +335,7 @@
   1.179    a theory where the user is looking are checked, while other parts
   1.180    that are presently not required are ignored.  The perspective is
   1.181    changed by opening or closing text area windows, or scrolling within
   1.182 -  some window.
   1.183 +  an editor window.
   1.184  
   1.185    The \emph{Theories} panel provides some further options to influence
   1.186    the process of continuous checking: it may be switched off globally
   1.187 @@ -366,20 +371,20 @@
   1.188    warnings, errors etc.\ (see also \figref{fig:output}).  In the
   1.189    latter case, the corresponding messages are shown by hovering with
   1.190    the mouse over the highlighted text --- although in many situations
   1.191 -  the user should already get some clue by looking at the text
   1.192 -  highlighting alone.
   1.193 +  the user should already get some clue by looking at the position of
   1.194 +  the text highlighting.
   1.195  
   1.196    \begin{figure}[htb]
   1.197    \begin{center}
   1.198    \includegraphics[scale=0.3]{output}
   1.199    \end{center}
   1.200 -  \caption{Multiple views on prover output: gutter area, text area
   1.201 -    with popup, overview area, Theories panel, Output panel}
   1.202 +  \caption{Multiple views on prover output: gutter area with icon,
   1.203 +    text area with popup, overview area, Theories panel, Output panel}
   1.204    \label{fig:output}
   1.205    \end{figure}
   1.206  
   1.207    The ``gutter area'' on the left-hand-side of the text area uses
   1.208 -  icons to provide a summary of the messages within the corresponding
   1.209 +  icons to provide a summary of the messages within the adjacent
   1.210    line of text.  Message priorities are used to prefer errors over
   1.211    warnings, warnings over information messages etc.  Plain output is
   1.212    ignored here.
   1.213 @@ -389,24 +394,27 @@
   1.214    of the whole text buffer.  The graphics is scaled to fit the logical
   1.215    buffer length into the given window height.  Mouse clicks on the
   1.216    overview area position the cursor approximately to the corresponding
   1.217 -  line of text in the buffer.
   1.218 +  line of text in the buffer.  Repainting the overview in real-time
   1.219 +  causes problems with big theories, so it is restricted to part of
   1.220 +  the text according to \emph{Plugin Options / Isabelle / General /
   1.221 +  Text Overview Limit} (in characters).
   1.222  
   1.223    Another course-grained overview is provided by the \emph{Theories}
   1.224 -  panel (\secref{sec:buffers-theories}), but without direct
   1.225 -  correspondence to text positions.  A double-click on one of the
   1.226 -  theory entries with their status overview opens the corresponding
   1.227 -  text buffer, without changing the cursor position.
   1.228 +  panel, but without direct correspondence to text positions.  A
   1.229 +  double-click on one of the theory entries with their status overview
   1.230 +  opens the corresponding text buffer, without changing the cursor
   1.231 +  position.
   1.232  
   1.233    \medskip In addition, the \emph{Output} panel displays prover
   1.234    messages that correspond to a given command, within a separate
   1.235    window.
   1.236  
   1.237    The cursor position in the presently active text area determines the
   1.238 -  prover commands whose cumulative message output is appended an shown
   1.239 -  in that window (in canonical order according to the processing of
   1.240 -  the command).  There are also control elements to modify the update
   1.241 -  policy of the output wrt.\ continued editor movements.  This is
   1.242 -  particularly useful with several independent instances of the
   1.243 +  prover commands whose cumulative message output is appended and
   1.244 +  shown in that window (in canonical order according to the processing
   1.245 +  of the command).  There are also control elements to modify the
   1.246 +  update policy of the output wrt.\ continued editor movements.  This
   1.247 +  is particularly useful with several independent instances of the
   1.248    \emph{Output} panel, which the Dockable Window Manager of jEdit can
   1.249    handle conveniently.
   1.250  
   1.251 @@ -414,7 +422,7 @@
   1.252    might find a separate window for prover messages familiar, but it is
   1.253    important to understand that the main Prover IDE feedback happens
   1.254    elsewhere.  It is possible to do meaningful proof editing
   1.255 -  efficiently while using the secondary window only rarely.
   1.256 +  efficiently, using secondary output windows only rarely.
   1.257  
   1.258    The main purpose of the output window is to ``debug'' unclear
   1.259    situations by inspecting internal state of the prover.\footnote{In
   1.260 @@ -462,36 +470,35 @@
   1.261  
   1.262    The tooltip popup window provides some controls to \emph{close} or
   1.263    \emph{detach} the window, turning it into a separate \emph{Info}
   1.264 -  dockable window managed by jEdit.  The @{verbatim ESCAPE} key closes
   1.265 +  window managed by jEdit.  The @{verbatim ESCAPE} key closes
   1.266    \emph{all} popups, which is particularly relevant when nested
   1.267    tooltips are stacking up.
   1.268  
   1.269    \medskip A black rectangle in the text indicates a hyperlink that
   1.270    may be followed by a mouse click (while the @{verbatim CONTROL} or
   1.271    @{verbatim COMMAND} modifier key is still pressed). Presently
   1.272 -  (Isabelle2013-1) there is no systematic way to return to the
   1.273 -  original location within the editor.
   1.274 +  (Isabelle2013-1) there is no systematic navigation within the
   1.275 +  editor to return to the original location.
   1.276  
   1.277    Also note that the link target may be a file that is itself not
   1.278    subject to formal document processing of the editor session and thus
   1.279    prevents further exploration: the chain of hyperlinks may end in
   1.280 -  some source file of the underlying logic image, even within the
   1.281 -  Isabelle/ML bootstrap sources of Isabelle/Pure, where the formal
   1.282 -  markup is less detailed. *}
   1.283 +  some source file of the underlying logic image, or within the
   1.284 +  Isabelle/ML bootstrap sources of Isabelle/Pure. *}
   1.285  
   1.286  
   1.287  section {* Text completion \label{sec:completion} *}
   1.288  
   1.289  text {* \paragraph{Completion tables} are determined statically from
   1.290    the ``outer syntax'' of the underlying edit mode (for theory files
   1.291 -  this is the syntax of Isar commands) and specifications of Isabelle
   1.292 +  this is the syntax of Isar commands), and specifications of Isabelle
   1.293    symbols (see also \secref{sec:symbols}).
   1.294  
   1.295    Symbols are completed in backslashed forms, e.g.\ @{verbatim
   1.296    "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the
   1.297    Isabelle symbol @{text "\<forall>"} in its Unicode rendering.\footnote{The
   1.298    extra backslash avoids overlap with keywords of the buffer syntax,
   1.299 -  and facilitates to produce Isabelle symbols in arbitrary syntactic
   1.300 +  and allows to produce Isabelle symbols robustly in most syntactic
   1.301    contexts.}  Alternatively, symbol abbreviations may be used as
   1.302    specified in @{file "$ISABELLE_HOME/etc/symbols"}.
   1.303  
   1.304 @@ -510,6 +517,7 @@
   1.305  
   1.306    \medskip
   1.307    \begin{tabular}{ll}
   1.308 +  \textbf{key} & \textbf{action} \\\hline
   1.309    @{verbatim "TAB"} & select completion \\
   1.310    @{verbatim "ESCAPE"} & dismiss popup \\
   1.311    @{verbatim "UP"} & move up one item \\
   1.312 @@ -523,19 +531,20 @@
   1.313    Otherwise the corresponding key event retains its standard meaning
   1.314    within the underlying text area.
   1.315  
   1.316 -  \paragraph{Explicit completion} is triggered by the keyword shortcut
   1.317 -  @{verbatim "C+b"} for action @{verbatim "isabelle.complete"}.  This
   1.318 -  overrides the original jEdit action @{verbatim "complete-word"} on
   1.319 -  that key sequence, but the latter is used as fall-back for
   1.320 +  \paragraph{Explicit completion} is triggered by the keyboard
   1.321 +  shortcut @{verbatim "C+b"} (action @{verbatim "isabelle.complete"}).
   1.322 +  This overrides the original jEdit binding for action @{verbatim
   1.323 +  "complete-word"}, but the latter is used as fall-back for
   1.324    non-Isabelle edit modes.  It is also possible to restore the
   1.325 -  original jEdit keyboard mapping of @{verbatim "complete-word"}.
   1.326 +  original jEdit keyboard mapping of @{verbatim "complete-word"} via
   1.327 +  \emph{Global Options / Shortcuts}.
   1.328  
   1.329    Replacement text is inserted immediately into the buffer, unless
   1.330    ambiguous results demand an explicit popup.
   1.331  
   1.332    \paragraph{Implicit completion} is triggered by regular keyboard
   1.333    input events during of the editing process in the main jEdit text
   1.334 -  area (and a few additional text fields like the search criterium of
   1.335 +  area (and a few additional text fields like the search criteria of
   1.336    the Find panel, see \secref{sec:find}).  Implicit completion depends
   1.337    on on further side-conditions:
   1.338  
   1.339 @@ -544,42 +553,44 @@
   1.340    \item The system option @{system_option jedit_completion} needs to
   1.341    be enabled (default).
   1.342  
   1.343 -  \item Completion of syntax keywords requires at least 3 characters
   1.344 -  in the text.
   1.345 +  \item Completion of syntax keywords requires at least 3 relevant
   1.346 +  characters in the text.
   1.347  
   1.348 -  \item The system option @{system_option jedit_completion} determines
   1.349 -  an additional delay (0.0 by default), before opening a completion
   1.350 -  popup.
   1.351 +  \item The system option @{system_option jedit_completion_delay}
   1.352 +  determines an additional delay (0.0 by default), before opening a
   1.353 +  completion popup.
   1.354  
   1.355    \item The system option @{system_option jedit_completion_immediate}
   1.356    (disabled by default) controls whether replacement text should be
   1.357 -  inserted immediately without popup, if possible.  This only works
   1.358 -  for Isabelle symbols (\secref{sec:symbols}).
   1.359 +  inserted immediately without popup.  This is restricted to Isabelle
   1.360 +  symbols and their abbreviations (\secref{sec:symbols}) --- plain
   1.361 +  keywords always demand a popup for clarity.
   1.362  
   1.363 -  \item Completion of symbol abbreviations with only 1 character in
   1.364 -  the text always enforces and explicit popup, independently of
   1.365 -  @{system_option jedit_completion_immediate}.
   1.366 +  \item Completion of symbol abbreviations with only one relevant
   1.367 +  character in the text always enforces an explicit popup,
   1.368 +  independently of @{system_option jedit_completion_immediate}.
   1.369  
   1.370    \end{enumerate}
   1.371  
   1.372    These completion options may be configured in \emph{Plugin Options /
   1.373    Isabelle / General / Completion}.  The default is quite moderate in
   1.374    showing occasional popups and refraining from immediate insertion.
   1.375 -  An additional of e.g.\ 0.3 seconds will make it even less ambitious.
   1.376 +  An additional completion delay of 0.3 seconds will make it even less
   1.377 +  ambitious.
   1.378  
   1.379 -  A more aggressive configuration is @{system_option
   1.380 +  In contrast, more aggressive completion works via @{system_option
   1.381    jedit_completion_delay}~@{verbatim "= 0.0"} and @{system_option
   1.382    jedit_completion_immediate}~@{verbatim "= true"}.  Thus the editing
   1.383 -  process becomes more dependent on the system guessing correctly what
   1.384 -  the user had in mind.  It requires some practice and study of the
   1.385 -  symbol abbreviation tables to be productive in this mode.
   1.386 +  process becomes dependent on the system guessing correctly what the
   1.387 +  user had in mind.  It requires some practice (and study of the
   1.388 +  symbol abbreviation tables) to become productive in this advanced
   1.389 +  mode.
   1.390  
   1.391 -  Unintended completions can be reverted by the regular @{verbatim
   1.392 -  undo} operation of jEdit.  When editing embedded languages such as
   1.393 -  ML works, it is better to disable either @{system_option
   1.394 +  In any case, unintended completions can be reverted by the regular
   1.395 +  @{verbatim undo} operation of jEdit.  When editing embedded
   1.396 +  languages such as ML, it is better to disable either @{system_option
   1.397    jedit_completion} or @{system_option jedit_completion_immediate}
   1.398 -  temporarily.
   1.399 -*}
   1.400 +  temporarily.  *}
   1.401  
   1.402  
   1.403  section {* Isabelle symbols \label{sec:symbols} *}
   1.404 @@ -587,11 +598,11 @@
   1.405  text {* Isabelle sources consist of \emph{symbols} that extend plain
   1.406    ASCII to allow infinitely many mathematical symbols within the
   1.407    formal sources.  This works without depending on particular
   1.408 -  encodings or varying Unicode standards
   1.409 +  encodings and varying Unicode standards
   1.410    \cite{Wenzel:2011:CICM}.\footnote{Raw Unicode characters within
   1.411    formal sources would compromise portability and reliability in the
   1.412 -  face of changing interpretation of various unexpected features of
   1.413 -  Unicode.}
   1.414 +  face of changing interpretation of special features of Unicode, such
   1.415 +  as Combining Characters or Bi-directional Text.}
   1.416  
   1.417    For the prover back-end, formal text consists of ASCII characters
   1.418    that are grouped according to some simple rules, e.g.\ as plain
   1.419 @@ -602,14 +613,16 @@
   1.420    as ``@{text "\<alpha>"}'', for example.  This symbol interpretation is
   1.421    specified by the Isabelle system distribution in @{file
   1.422    "$ISABELLE_HOME/etc/symbols"} and may be augmented by the user in
   1.423 -  @{verbatim "$ISABELLE_HOME_USER/etc/symbols"}.
   1.424 +  @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"}.
   1.425  
   1.426    The appendix of \cite{isabelle-isar-ref} gives an overview of the
   1.427    standard interpretation of finitely many symbols from the infinite
   1.428    collection.  Uninterpreted symbols are displayed literally, e.g.\
   1.429    ``@{verbatim "\<foobar>"}''.  Overlap of Unicode characters used in
   1.430 -  symbol interpretation with informal ones that might appear e.g.\ in
   1.431 -  comments needs to be avoided!
   1.432 +  symbol interpretation with informal ones (which might appear e.g.\
   1.433 +  in comments) needs to be avoided!  Raw Unicode characters within
   1.434 +  prover source files should be restricted to informal parts, e.g.\ to
   1.435 +  write text in non-latin alphabets in comments.
   1.436  
   1.437    \medskip \paragraph{Encoding.} Technically, the Unicode view on
   1.438    Isabelle symbols is an \emph{encoding} in jEdit (not in the
   1.439 @@ -632,13 +645,15 @@
   1.440    screen (or printer).
   1.441  
   1.442    Note that a Java/AWT/Swing application can load additional fonts
   1.443 -  only if they are not installed as system font already!  This means
   1.444 -  some old version of @{verbatim IsabelleText} that happens to be
   1.445 -  already present prevents Isabelle/jEdit from using its current
   1.446 -  bundled version.  This results in missing glyphs (black rectangles),
   1.447 -  when some obsolete version of @{verbatim IsabelleText} is used by
   1.448 -  accident.  This problem can be avoided by refraining to ``install''
   1.449 -  any version of @{verbatim IsabelleText} in the first place.
   1.450 +  only if they are not installed on the operating system already!
   1.451 +  Some old version of @{verbatim IsabelleText} that happens to be
   1.452 +  provided by the operating system would prevents Isabelle/jEdit from
   1.453 +  its bundled version.  This could lead to missing glyphs (black
   1.454 +  rectangles), when the system version of @{verbatim IsabelleText} is
   1.455 +  older than the application version.  This problem can be avoided by
   1.456 +  refraining to ``install'' any version of @{verbatim IsabelleText} in
   1.457 +  the first place (although it might be occasionally tempting to use
   1.458 +  the same font in other applications).
   1.459  
   1.460    \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit
   1.461    could delegate the problem to produce Isabelle symbols in their
   1.462 @@ -656,7 +671,7 @@
   1.463  
   1.464    \item The \emph{Symbols} panel with some GUI buttons to insert
   1.465    certain symbols in the text buffer.  There are also tooltips to
   1.466 -  reveal to official Isabelle representation with some additional
   1.467 +  reveal the official Isabelle representation with some additional
   1.468    information about \emph{symbol abbreviations} (see below).
   1.469  
   1.470    \item Copy / paste from decoded source files: text that is rendered
   1.471 @@ -668,7 +683,7 @@
   1.472    \item Copy / paste from prover output within Isabelle/jEdit.  The
   1.473    same principles as for text buffers apply, but note that \emph{copy}
   1.474    in secondary Isabelle/jEdit windows works via the keyboard shortcut
   1.475 -  @{verbatim "C+c"}.  The jEdit menu actions always refer to the
   1.476 +  @{verbatim "C+c"}, while jEdit menu actions always refer to the
   1.477    primary text area!
   1.478  
   1.479    \item Completion provided by Isabelle plugin (see
   1.480 @@ -684,23 +699,21 @@
   1.481  
   1.482    \medskip
   1.483    \begin{tabular}{lll}
   1.484 -    \textbf{symbol} & \textbf{abbreviation} & \textbf{backslashed name} \\\hline
   1.485 -    @{text "\<lambda>"}   & @{verbatim "%"}     &  @{verbatim "\\lambda"}         \\
   1.486 -    @{text "\<Rightarrow>"}  & @{verbatim "=>"}    &  @{verbatim "\\Rightarrow"}     \\
   1.487 -    @{text "\<Longrightarrow>"} & @{verbatim "==>"}   &  @{verbatim "\\Longrightarrow"} \\
   1.488 -
   1.489 -    @{text "\<And>"}  & @{verbatim "!!"}    &  @{verbatim "\\And"}            \\
   1.490 -    @{text "\<equiv>"}  & @{verbatim "=="}    &  @{verbatim "\\equiv"}          \\
   1.491 -
   1.492 -    @{text "\<forall>"}   & @{verbatim "!"}     &  @{verbatim "\\forall"}         \\
   1.493 -    @{text "\<exists>"}   & @{verbatim "?"}     &  @{verbatim "\\exists"}         \\
   1.494 -    @{text "\<longrightarrow>"} & @{verbatim "-->"}   &  @{verbatim "\\longrightarrow"} \\
   1.495 -    @{text "\<and>"}   & @{verbatim "&"}     &  @{verbatim "\\and"}            \\
   1.496 -    @{text "\<or>"}   & @{verbatim "|"}     &  @{verbatim "\\or"}             \\
   1.497 -    @{text "\<not>"}   & @{verbatim "~"}     &  @{verbatim "\\not"}            \\
   1.498 -    @{text "\<noteq>"}   & @{verbatim "~="}    &  @{verbatim "\\noteq"}          \\
   1.499 -    @{text "\<in>"}   & @{verbatim ":"}     &  @{verbatim "\\in"}             \\
   1.500 -    @{text "\<notin>"}   & @{verbatim "~:"}    &  @{verbatim "\\notin"}          \\
   1.501 +    \textbf{symbol} & \textbf{backslashed name} & \textbf{abbreviation} \\\hline
   1.502 +    @{text "\<lambda>"} & @{verbatim "\\lambda"} & @{verbatim "%"} \\
   1.503 +    @{text "\<Rightarrow>"} & @{verbatim "\\Rightarrow"} & @{verbatim "=>"} \\
   1.504 +    @{text "\<Longrightarrow>"} & @{verbatim "\\Longrightarrow"} & @{verbatim "==>"} \\[0.5ex]
   1.505 +    @{text "\<And>"} & @{verbatim "\\And"} & @{verbatim "!!"} \\
   1.506 +    @{text "\<equiv>"} & @{verbatim "\\equiv"} & @{verbatim "=="} \\[0.5ex]
   1.507 +    @{text "\<forall>"} & @{verbatim "\\forall"} & @{verbatim "!"} \\
   1.508 +    @{text "\<exists>"} & @{verbatim "\\exists"} & @{verbatim "?"} \\
   1.509 +    @{text "\<longrightarrow>"} & @{verbatim "\\longrightarrow"} & @{verbatim "-->"} \\
   1.510 +    @{text "\<and>"} & @{verbatim "\\and"} & @{verbatim "&"} \\
   1.511 +    @{text "\<or>"} & @{verbatim "\\or"} & @{verbatim "|"} \\
   1.512 +    @{text "\<not>"} & @{verbatim "\\not"} & @{verbatim "~"} \\
   1.513 +    @{text "\<noteq>"} & @{verbatim "\\noteq"} & @{verbatim "~="} \\
   1.514 +    @{text "\<in>"} & @{verbatim "\\in"} & @{verbatim ":"} \\
   1.515 +    @{text "\<notin>"} & @{verbatim "\\notin"} & @{verbatim "~:"} \\
   1.516    \end{tabular}
   1.517    \medskip
   1.518  
   1.519 @@ -708,27 +721,27 @@
   1.520    logical notation provides ASCII alternatives that often coincide,
   1.521    but deviate occasionally.  This occasionally causes user confusion
   1.522    with very old-fashioned Isabelle source that use ASCII replacement
   1.523 -  notation like @{verbatim "!"} or @{verbatim "ALL"} directly.
   1.524 +  notation like @{verbatim "!"} or @{verbatim "ALL"} directly in the
   1.525 +  text.
   1.526 +
   1.527 +  On the other hand, coincidence of symbol abbreviations with ASCII
   1.528 +  replacement syntax syntax helps to update old theory sources via
   1.529 +  explicit completion (see also @{verbatim "C+b"} explained in
   1.530 +  \secref{sec:completion}).
   1.531  
   1.532    \end{enumerate}
   1.533  
   1.534 -  Raw Unicode characters within prover source files should be
   1.535 -  restricted to informal parts, e.g.\ to write text in non-latin
   1.536 -  alphabets.  Mathematical symbols should be defined via the official
   1.537 -  rendering tables, to avoid problems with portability and long-term
   1.538 -  storage of formal text.
   1.539 -
   1.540    \paragraph{Control symbols.} There are some special control symbols
   1.541 -  to modify the style of a single symbol (without nesting). Control
   1.542 -  symbols may be applied to a region of selected text, either using
   1.543 -  the \emph{Symbols} panel or keyboard shortcuts or jEdit actions.
   1.544 -  These editor operations produce a separate control symbol for each
   1.545 -  symbol in the text, in order to make the whole text appear in a
   1.546 -  certain style.
   1.547 +  to modify the display style of a single symbol (without
   1.548 +  nesting). Control symbols may be applied to a region of selected
   1.549 +  text, either using the \emph{Symbols} panel or keyboard shortcuts or
   1.550 +  jEdit actions.  These editor operations produce a separate control
   1.551 +  symbol for each symbol in the text, in order to make the whole text
   1.552 +  appear in a certain style.
   1.553  
   1.554    \medskip
   1.555    \begin{tabular}{llll}
   1.556 -    style & \textbf{symbol} & shortcut & action \\\hline
   1.557 +    \textbf{style} & \textbf{symbol} & \textbf{shortcut} & \textbf{action} \\\hline
   1.558      superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{verbatim "isabelle.control-sup"} \\
   1.559      subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{verbatim "isabelle.control-sub"} \\
   1.560      bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{verbatim "isabelle.control-bold"} \\
   1.561 @@ -758,7 +771,7 @@
   1.562    \emph{information messages}, which are indicated in the text area by
   1.563    blue squiggles and a blue information sign in the gutter (see
   1.564    \figref{fig:auto-tools}).  The message content may be shown as for
   1.565 -  any other message, see also \secref{sec:prover-output}.  Some tools
   1.566 +  other output (see also \secref{sec:prover-output}).  Some tools
   1.567    produce output with \emph{sendback} markup, which means that
   1.568    clicking on certain parts of the output inserts that text into the
   1.569    source in the proper place.
   1.570 @@ -771,7 +784,7 @@
   1.571    \label{fig:auto-tools}
   1.572    \end{figure}
   1.573  
   1.574 -  \medskip The following Isabelle system options control the behaviour
   1.575 +  \medskip The following Isabelle system options control the behavior
   1.576    of automatically tried tools (see also the jEdit dialog window
   1.577    \emph{Plugin Options / Isabelle / General / Automatically tried
   1.578    tools}):
   1.579 @@ -780,7 +793,7 @@
   1.580  
   1.581    \item @{system_option auto_methods} controls automatic use of a
   1.582    combination of standard proof methods (@{method auto}, @{method
   1.583 -  simp}, @{method blast}, etc.).  This corresponds to the command
   1.584 +  simp}, @{method blast}, etc.).  This corresponds to the Isar command
   1.585    @{command "try0"}.
   1.586  
   1.587    The tool is disabled by default, since unparameterized invocation of
   1.588 @@ -826,7 +839,7 @@
   1.589    \begin{itemize}
   1.590  
   1.591    \item @{system_option auto_time_limit} (default 2.0) determines the
   1.592 -  timeout (in seconds) for each tool execution individually.
   1.593 +  timeout (in seconds) for each tool execution.
   1.594  
   1.595    \item @{system_option auto_time_start} (default 1.0) determines the
   1.596    start delay (in seconds) for automatically tried tools, after the
   1.597 @@ -843,18 +856,19 @@
   1.598  
   1.599    Users should experiment how the available CPU resources (number of
   1.600    cores) are best invested to get additional feedback from prover in
   1.601 -  the background, by using weaker or stronger tools.  *}
   1.602 +  the background, by using a selection of weaker or stronger tools.
   1.603 +*}
   1.604  
   1.605  
   1.606  section {* Sledgehammer \label{sec:sledgehammer} *}
   1.607  
   1.608  text {* The \emph{Sledgehammer} panel (\figref{fig:sledgehammer})
   1.609 -  provides a view on some independent execution of @{command
   1.610 -  sledgehammer}, with process indicator (spinning wheel) and GUI
   1.611 -  elements for important Sledgehammer arguments and options.  Any
   1.612 +  provides a view on some independent execution of the Isar command
   1.613 +  @{command sledgehammer}, with process indicator (spinning wheel) and
   1.614 +  GUI elements for important Sledgehammer arguments and options.  Any
   1.615    number of Sledgehammer panels may be active, according to the
   1.616 -  standard policies of Dockable Window Management in jEdit.  Closing a
   1.617 -  window also cancels the corresponding prover tasks.
   1.618 +  standard policies of Dockable Window Management in jEdit.  Closing
   1.619 +  such windows also cancels the corresponding prover tasks.
   1.620  
   1.621    \begin{figure}[htb]
   1.622    \begin{center}
   1.623 @@ -871,7 +885,7 @@
   1.624    process.
   1.625  
   1.626    Results appear incrementally in the output window of the panel.
   1.627 -  Proposed proof snippets are marked up as \emph{sendback}, which
   1.628 +  Proposed proof snippets are marked-up as \emph{sendback}, which
   1.629    means a single mouse click inserts the text into a suitable place of
   1.630    the original source.  Some manual editing may be required
   1.631    nonetheless, say to remove earlier proof attempts. *}
   1.632 @@ -880,10 +894,10 @@
   1.633  section {* Find theorems \label{sec:find} *}
   1.634  
   1.635  text {* The \emph{Find} panel (\figref{fig:find}) provides an
   1.636 -  independent view for @{command find_theorems}.  The main text field
   1.637 -  accepts search criteria according to the syntax @{syntax
   1.638 -  thmcriterium} given in \cite{isabelle-isar-ref}.  Further options of
   1.639 -  @{command find_theorems} are available via GUI elements.
   1.640 +  independent view for the Isar command @{command find_theorems}.  The
   1.641 +  main text field accepts search criteria according to the syntax
   1.642 +  @{syntax thmcriterium} given in \cite{isabelle-isar-ref}.  Further
   1.643 +  options of @{command find_theorems} are available via GUI elements.
   1.644  
   1.645    \begin{figure}[htb]
   1.646    \begin{center}
   1.647 @@ -908,7 +922,8 @@
   1.648  
   1.649    Isabelle/jEdit provides SideKick parsers for its main mode for
   1.650    theory files, as well as some minor modes for the @{verbatim NEWS}
   1.651 -  file, session @{verbatim ROOT} files, and @{verbatim options}.
   1.652 +  file, session @{verbatim ROOT} files, and system @{verbatim
   1.653 +  options}.
   1.654  
   1.655    Moreover, the special SideKick parser @{verbatim "isabelle-markup"}
   1.656    provides access to the full (uninterpreted) markup tree of the PIDE
   1.657 @@ -953,17 +968,17 @@
   1.658    considerable runtime itself --- on the Java Virtual Machine that
   1.659    runs Isabelle/Scala, not Isabelle/ML.  Internally, the
   1.660    Isabelle/Scala module @{verbatim isabelle.ML_Statistics} provides
   1.661 -  further access runtime statistics of Isabelle/ML.  *}
   1.662 +  further access to statistics of Isabelle/ML.  *}
   1.663  
   1.664  
   1.665  section {* Isabelle/Scala console *}
   1.666  
   1.667  text {* The \emph{Console} plugin of jEdit manages various shells
   1.668    (command interpreters), e.g.\ \emph{BeanShell}, which is the
   1.669 -  official jEdit scripting language, and the somewhat
   1.670 -  platform-independent \emph{System} shell.  Thus the console provides
   1.671 -  similar functionality than the special buffers @{verbatim
   1.672 -  "*scratch*"} and @{verbatim "*shell*"} in Emacs.
   1.673 +  official jEdit scripting language, and the cross-platform
   1.674 +  \emph{System} shell.  Thus the console provides similar
   1.675 +  functionality than the special buffers @{verbatim "*scratch*"} and
   1.676 +  @{verbatim "*shell*"} in Emacs.
   1.677  
   1.678    Isabelle/jEdit extends the repertoire of the console by
   1.679    \emph{Scala}, which is the regular Scala toplevel loop running
   1.680 @@ -988,7 +1003,7 @@
   1.681  section {* Low-level output *}
   1.682  
   1.683  text {* Prover output is normally shown directly in the main text area
   1.684 -  or adjacent \emph{Output} panels, as explained in
   1.685 +  or secondary \emph{Output} panels, as explained in
   1.686    \secref{sec:prover-output}.
   1.687  
   1.688    Beyond this, it is occasionally useful to inspect low-level output
   1.689 @@ -1002,8 +1017,8 @@
   1.690    corresponding dockable window; earlier messages are lost.
   1.691  
   1.692    Actual display of protocol messages causes considerable slowdown, so
   1.693 -  it is important to ``undock'' the \emph{Protocol} panel for
   1.694 -  production work.
   1.695 +  it is important to undock all \emph{Protocol} panels for production
   1.696 +  work.
   1.697  
   1.698    \item \emph{Raw Output} shows chunks of text from the @{verbatim
   1.699    stdout} and @{verbatim stderr} channels of the prover process.
   1.700 @@ -1051,7 +1066,8 @@
   1.701    \item \textbf{Problem:} Odd behavior of some diagnostic commands with
   1.702    global side-effects, like writing a physical file.
   1.703  
   1.704 -  \textbf{Workaround:} Avoid such commands.
   1.705 +  \textbf{Workaround:} Copy / paste complete command text from
   1.706 +  elsewhere, or discontinue continuous checking temporarily.
   1.707  
   1.708    \item \textbf{Problem:} No way to delete document nodes from the overall
   1.709    collection of theories.
   1.710 @@ -1063,16 +1079,17 @@
   1.711    @{verbatim "C+MINUS"} for adjusting the editor font size depend on
   1.712    platform details and national keyboards.
   1.713  
   1.714 -  \textbf{Workaround:} Use numeric keypad or rebind keys in the
   1.715 -  jEdit Shortcuts options dialog.
   1.716 +  \textbf{Workaround:} Rebind keys via \emph{Global Options /
   1.717 +  Shortcuts}.
   1.718  
   1.719    \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
   1.720    "COMMAND+COMMA"} for application \emph{Preferences} is in conflict
   1.721    with the jEdit default shortcut for \emph{Incremental Search Bar}
   1.722    (action @{verbatim "quick-search"}).
   1.723  
   1.724 -  \textbf{Workaround:} Remap in jEdit manually according to national
   1.725 -  keyboard, e.g.\ @{verbatim "COMMAND+SLASH"} on English ones.
   1.726 +  \textbf{Workaround:} Rebind key via \emph{Global Options /
   1.727 +  Shortcuts} according to national keyboard, e.g.\ @{verbatim
   1.728 +  "COMMAND+SLASH"} on English ones.
   1.729  
   1.730    \item \textbf{Problem:} Mac OS X system fonts sometimes lead to
   1.731    character drop-outs in the main text area.
   1.732 @@ -1105,7 +1122,7 @@
   1.733    Windows, but not on Mac OS X or various Linux / X11 window managers.
   1.734  
   1.735    \textbf{Workaround:} Use native full-screen control of the window
   1.736 -  manager, if available (notably on Mac OS X).
   1.737 +  manager (notably on Mac OS X).
   1.738  
   1.739    \item \textbf{Problem:} Full-screen mode and dockable windows in
   1.740    \emph{floating} state may lead to confusion about window placement
     2.1 --- a/src/Doc/antiquote_setup.ML	Wed Nov 06 21:20:20 2013 +0100
     2.2 +++ b/src/Doc/antiquote_setup.ML	Thu Nov 07 13:34:04 2013 +0100
     2.3 @@ -47,6 +47,22 @@
     2.4      (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
     2.5  
     2.6  
     2.7 +(* unchecked file *)
     2.8 +
     2.9 +val file_unchecked_setup =
    2.10 +  Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
    2.11 +    (fn {context = ctxt, ...} => fn (name, pos) =>
    2.12 +      let
    2.13 +        val dir = Thy_Load.master_directory (Proof_Context.theory_of ctxt);
    2.14 +        val path = Path.append dir (Path.explode name);
    2.15 +        val _ = Position.report pos (Markup.path name);
    2.16 +      in
    2.17 +        space_explode "/" name
    2.18 +        |> map Thy_Output.verb_text
    2.19 +        |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
    2.20 +      end);
    2.21 +
    2.22 +
    2.23  (* ML text *)
    2.24  
    2.25  local
    2.26 @@ -233,6 +249,7 @@
    2.27  
    2.28  val setup =
    2.29    verbatim_setup #>
    2.30 +  file_unchecked_setup #>
    2.31    index_ml_setup #>
    2.32    named_thms_setup #>
    2.33    thy_file_setup #>