tuned;
authorwenzelm
Mon May 04 21:58:35 2015 +0200 (2015-05-04)
changeset 602579ed816c033c5
parent 60256 2925c5552e25
child 60258 7364d4316a56
tuned;
src/Doc/JEdit/JEdit.thy
src/Doc/manual.bib
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Mon May 04 20:16:19 2015 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon May 04 21:58:35 2015 +0200
     1.3 @@ -84,7 +84,7 @@
     1.4    application startup, the selected logic session image is provided
     1.5    automatically by the Isabelle build tool @{cite "isabelle-sys"}: if it is
     1.6    absent or outdated wrt.\ its sources, the build process updates it before
     1.7 -  entering the Prover IDE.  Changing the logic session within Isabelle/jEdit
     1.8 +  entering the Prover IDE.  Change of the logic session within Isabelle/jEdit
     1.9    requires a restart of the whole application.
    1.10  
    1.11    \medskip The main job of the Prover IDE is to manage sources and their
    1.12 @@ -103,7 +103,8 @@
    1.13  
    1.14    Thus the Prover IDE gives an impression of direct access to formal content
    1.15    of the prover within the editor, but in reality only certain aspects are
    1.16 -  exposed, according to the possibilities of the prover and its many tools.
    1.17 +  exposed, according to the possibilities of the prover and its many add-on
    1.18 +  tools.
    1.19  \<close>
    1.20  
    1.21  
    1.22 @@ -311,7 +312,7 @@
    1.23    in mind that this extra variance of GUI functionality is unlikely to
    1.24    work in arbitrary combinations.  The platform-independent
    1.25    \emph{Nimbus} and \emph{Metal} should always work.  The historic
    1.26 -  \emph{CDE/Motif} is better avoided.
    1.27 +  \emph{CDE/Motif} is better ignore altogether.
    1.28  
    1.29    After changing the look-and-feel in \emph{Global Options~/
    1.30    Appearance}, it is advisable to restart Isabelle/jEdit in order to
    1.31 @@ -336,10 +337,10 @@
    1.32    \emph{HyperSearch Results} or the \emph{File System Browser}. Plugins often
    1.33    provide a central dockable to access their key functionality, which may be
    1.34    opened by the user on demand. The Isabelle/jEdit plugin takes this approach
    1.35 -  to the extreme: its plugin menu merely provides entry-points to panels that
    1.36 -  are managed as dockable windows. Some important panels are docked by
    1.37 +  to the extreme: its plugin menu provides the entry-points to many panels
    1.38 +  that are managed as dockable windows. Some important panels are docked by
    1.39    default, e.g.\ \emph{Documentation}, \emph{Output}, \emph{Query}, but the
    1.40 -  user can change this arrangement easily.
    1.41 +  user can change this arrangement easily and persistently.
    1.42  
    1.43    Compared to plain jEdit, dockable window management in Isabelle/jEdit is
    1.44    slightly augmented according to the the following principles:
    1.45 @@ -401,15 +402,15 @@
    1.46    alphabets in comments.
    1.47  
    1.48    \medskip \paragraph{Encoding.} Technically, the Unicode view on Isabelle
    1.49 -  symbols is an \emph{encoding} in jEdit (not in the underlying JVM) that is
    1.50 -  called @{verbatim "UTF-8-Isabelle"}. It is provided by the Isabelle/jEdit
    1.51 -  plugin and enabled by default for all source files. Sometimes such defaults
    1.52 -  are reset accidentally, or malformed UTF-8 sequences in the text force jEdit
    1.53 -  to fall back on a different encoding like @{verbatim "ISO-8859-15"}. In that
    1.54 -  case, verbatim ``@{verbatim "\<alpha>"}'' will be shown in the text buffer instead
    1.55 -  of its Unicode rendering ``@{text "\<alpha>"}''. The jEdit menu operation
    1.56 -  \emph{File~/ Reload with Encoding~/ UTF-8-Isabelle} helps to resolve such
    1.57 -  problems (after repairing malformed parts of the text).
    1.58 +  symbols is an \emph{encoding} called @{verbatim "UTF-8-Isabelle"} in jEdit
    1.59 +  (not in the underlying JVM). It is provided by the Isabelle/jEdit plugin and
    1.60 +  enabled by default for all source files. Sometimes such defaults are reset
    1.61 +  accidentally, or malformed UTF-8 sequences in the text force jEdit to fall
    1.62 +  back on a different encoding like @{verbatim "ISO-8859-15"}. In that case,
    1.63 +  verbatim ``@{verbatim "\<alpha>"}'' will be shown in the text buffer instead of its
    1.64 +  Unicode rendering ``@{text "\<alpha>"}''. The jEdit menu operation \emph{File~/
    1.65 +  Reload with Encoding~/ UTF-8-Isabelle} helps to resolve such problems (after
    1.66 +  repairing malformed parts of the text).
    1.67  
    1.68    \medskip \paragraph{Font.} Correct rendering via Unicode requires a
    1.69    font that contains glyphs for the corresponding codepoints.  Most
    1.70 @@ -453,11 +454,11 @@
    1.71    some web browser or mail client, as long as the same Unicode view on
    1.72    Isabelle symbols is used.
    1.73  
    1.74 -  \item Copy/paste from prover output within Isabelle/jEdit.  The
    1.75 -  same principles as for text buffers apply, but note that \emph{copy}
    1.76 -  in secondary Isabelle/jEdit windows works via the keyboard shortcut
    1.77 -  @{verbatim "C+c"}, while jEdit menu actions always refer to the
    1.78 -  primary text area!
    1.79 +  \item Copy/paste from prover output within Isabelle/jEdit. The same
    1.80 +  principles as for text buffers apply, but note that \emph{copy} in secondary
    1.81 +  Isabelle/jEdit windows works via the keyboard shortcuts @{verbatim "C+c"} or
    1.82 +  @{verbatim "C+INSERT"}, while jEdit menu actions always refer to the primary
    1.83 +  text area!
    1.84  
    1.85    \item Completion provided by Isabelle plugin (see
    1.86    \secref{sec:completion}).  Isabelle symbols have a canonical name
    1.87 @@ -595,9 +596,9 @@
    1.88    Despite the flexibility of URLs in jEdit, local files are particularly
    1.89    important and are accessible without protocol prefix. Here the path notation
    1.90    is that of the Java Virtual Machine on the underlying platform. On Windows
    1.91 -  the preferred form uses backslashes, but happens to accept forward slashes
    1.92 -  like Unix/POSIX. Further differences arise due to Windows drive letters and
    1.93 -  network shares.
    1.94 +  the preferred form uses backslashes, but happens to accept also forward
    1.95 +  slashes like Unix/POSIX. Further differences arise due to Windows drive
    1.96 +  letters and network shares.
    1.97  
    1.98    The Java notation for files needs to be distinguished from the one of
    1.99    Isabelle, which uses POSIX notation with forward slashes on \emph{all}
   1.100 @@ -614,8 +615,8 @@
   1.101    though, due to the bias of jEdit towards platform-specific notation and of
   1.102    Isabelle towards POSIX. Moreover, the Isabelle settings environment is not
   1.103    yet active when starting Isabelle/jEdit via its standard application
   1.104 -  wrapper, in contrast to @{verbatim "isabelle jedit"} run from the command
   1.105 -  line (\secref{sec:command-line}).
   1.106 +  wrapper, in contrast to @{tool jedit} run from the command line
   1.107 +  (\secref{sec:command-line}).
   1.108  
   1.109    Isabelle/jEdit imitates @{verbatim "$ISABELLE_HOME"} and @{verbatim
   1.110    "$ISABELLE_HOME_USER"} within the Java process environment, in order to
   1.111 @@ -687,7 +688,7 @@
   1.112  
   1.113    In any case, source files are managed by the PIDE infrastructure: the
   1.114    physical file-system only plays a subordinate role. The relevant version of
   1.115 -  source text is passed directly from the editor to the prover, via internal
   1.116 +  source text is passed directly from the editor to the prover, using internal
   1.117    communication channels.
   1.118  \<close>
   1.119  
   1.120 @@ -739,13 +740,14 @@
   1.121    rendering, based on a standard repertoire known from IDEs for programming
   1.122    languages: colors, icons, highlighting, squiggly underlines, tooltips,
   1.123    hyperlinks etc. For outer syntax of Isabelle/Isar there is some traditional
   1.124 -  syntax-highlighting via static keyword tables and tokenization within the
   1.125 -  editor. In contrast, the painting of inner syntax (term language etc.)\ uses
   1.126 -  semantic information that is reported dynamically from the logical context.
   1.127 -  Thus the prover can provide additional markup to help the user to understand
   1.128 -  the meaning of formal text, and to produce more text with some add-on tools
   1.129 -  (e.g.\ information messages with \emph{sendback} markup by automated provers
   1.130 -  or disprovers in the background).
   1.131 +  syntax-highlighting via static keywords and tokenization within the editor;
   1.132 +  this buffer syntax is determined from theory imports. In contrast, the
   1.133 +  painting of inner syntax (term language etc.)\ uses semantic information
   1.134 +  that is reported dynamically from the logical context. Thus the prover can
   1.135 +  provide additional markup to help the user to understand the meaning of
   1.136 +  formal text, and to produce more text with some add-on tools (e.g.\
   1.137 +  information messages with \emph{sendback} markup by automated provers or
   1.138 +  disprovers in the background).
   1.139  
   1.140  \<close>
   1.141  
   1.142 @@ -766,7 +768,7 @@
   1.143    document-model on demand, the first time when opened explicitly in the
   1.144    editor. There are further tricks to manage markup of ML files, such that
   1.145    Isabelle/HOL may be edited conveniently in the Prover IDE on small machines
   1.146 -  with only 4--8\,GB of main memory. Using @{verbatim Pure} as logic session
   1.147 +  with only 8\,GB of main memory. Using @{verbatim Pure} as logic session
   1.148    image, the exploration may start at the top @{file
   1.149    "$ISABELLE_HOME/src/HOL/Main.thy"} or the bottom @{file
   1.150    "$ISABELLE_HOME/src/HOL/HOL.thy"}, for example.
   1.151 @@ -1020,7 +1022,7 @@
   1.152    subject to formal document processing of the editor session and thus
   1.153    prevents further exploration: the chain of hyperlinks may end in
   1.154    some source file of the underlying logic image, or within the
   1.155 -  Isabelle/ML bootstrap sources of Isabelle/Pure.\<close>
   1.156 +  ML bootstrap sources of Isabelle/Pure.\<close>
   1.157  
   1.158  
   1.159  section \<open>Completion \label{sec:completion}\<close>
   1.160 @@ -1095,7 +1097,7 @@
   1.161  text \<open>
   1.162    Syntax completion tables are determined statically from the keywords of the
   1.163    ``outer syntax'' of the underlying edit mode: for theory files this is the
   1.164 -  syntax of Isar commands.
   1.165 +  syntax of Isar commands according to the cumulative theory imports.
   1.166  
   1.167    Keywords are usually plain words, which means the completion mechanism only
   1.168    inserts them directly into the text for explicit completion
   1.169 @@ -1384,7 +1386,7 @@
   1.170    \begin{itemize}
   1.171  
   1.172    \item @{system_option_def completion_limit} specifies the maximum number of
   1.173 -  name-space entries exposed in semantic completion by the prover.
   1.174 +  items for various semantic completion operations (name-space entries etc.)
   1.175  
   1.176    \item @{system_option_def jedit_completion} guards implicit completion via
   1.177    regular jEdit key events (\secref{sec:completion-input}): it allows to
   1.178 @@ -1598,9 +1600,9 @@
   1.179  section \<open>Citations and Bib{\TeX} entries\<close>
   1.180  
   1.181  text \<open>Citations are managed by {\LaTeX} and Bib{\TeX} in @{verbatim ".bib"}
   1.182 -  files. The Isabelle session build process and the
   1.183 -  @{verbatim "isabelle latex"} tool @{cite "isabelle-sys"} are smart enough
   1.184 -  to assemble the result, based on the session directory layout.
   1.185 +  files. The Isabelle session build process and the @{tool latex} tool @{cite
   1.186 +  "isabelle-sys"} are smart enough to assemble the result, based on the
   1.187 +  session directory layout.
   1.188  
   1.189    The document antiquotation @{text "@{cite}"} is described in @{cite
   1.190    "isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for
   1.191 @@ -1685,7 +1687,7 @@
   1.192    \begin{itemize}
   1.193  
   1.194    \item \emph{Protocol} shows internal messages between the
   1.195 -  Isabelle/Scala and Isabelle/ML side of the PIDE editing protocol.
   1.196 +  Isabelle/Scala and Isabelle/ML side of the PIDE document editing protocol.
   1.197    Recording of messages starts with the first activation of the
   1.198    corresponding dockable window; earlier messages are lost.
   1.199  
   1.200 @@ -1707,11 +1709,14 @@
   1.201    Under normal circumstances, prover output always works via managed message
   1.202    channels (corresponding to @{ML writeln}, @{ML warning}, @{ML
   1.203    Output.error_message} in Isabelle/ML), which are displayed by regular means
   1.204 -  within the document model (\secref{sec:output}).
   1.205 +  within the document model (\secref{sec:output}). Unhandled Isabelle/ML
   1.206 +  exceptions are printed by the system via @{ML Output.error_message}.
   1.207  
   1.208 -  \item \emph{Syslog} shows system messages that might be relevant to
   1.209 -  diagnose problems with the startup or shutdown phase of the prover
   1.210 -  process; this also includes raw output on @{verbatim stderr}.
   1.211 +  \item \emph{Syslog} shows system messages that might be relevant to diagnose
   1.212 +  problems with the startup or shutdown phase of the prover process; this also
   1.213 +  includes raw output on @{verbatim stderr}. Isabelle/ML also provides an
   1.214 +  explicit @{ML Output.system_message} operation, which is occasionally useful
   1.215 +  for diagnostic purposes within the system infrastructure itself.
   1.216  
   1.217    A limited amount of syslog messages are buffered, independently of
   1.218    the docking state of the \emph{Syslog} panel.  This allows to
   1.219 @@ -1778,9 +1783,9 @@
   1.220  
   1.221    \textbf{Workaround:} Use a regular re-parenting X11 window manager.
   1.222  
   1.223 -  \item \textbf{Problem:} Recent forks of Linux/X11 window managers
   1.224 -  and desktop environments (variants of Gnome) disrupt the handling of
   1.225 -  menu popups and mouse positions of Java/AWT/Swing.
   1.226 +  \item \textbf{Problem:} Various forks of Linux/X11 window managers and
   1.227 +  desktop environments (like Gnome) disrupt the handling of menu popups and
   1.228 +  mouse positions of Java/AWT/Swing.
   1.229  
   1.230    \textbf{Workaround:} Use mainstream versions of Linux desktops.
   1.231  
     2.1 --- a/src/Doc/manual.bib	Mon May 04 20:16:19 2015 +0200
     2.2 +++ b/src/Doc/manual.bib	Mon May 04 21:58:35 2015 +0200
     2.3 @@ -1957,7 +1957,7 @@
     2.4  @inproceedings{Wenzel:2013:ITP,
     2.5    author    = {Makarius Wenzel},
     2.6    title     = {Shared-Memory Multiprocessing for Interactive Theorem Proving},
     2.7 -  booktitle = {Interactive Theorem Proving - 4th International Conference,
     2.8 +  booktitle = {Interactive Theorem Proving --- 4th International Conference,
     2.9                 ITP 2013, Rennes, France, July 22-26, 2013. Proceedings},
    2.10    editor    = {Sandrine Blazy and
    2.11                 Christine Paulin-Mohring and
    2.12 @@ -1989,7 +1989,7 @@
    2.13    year = 2014,
    2.14    series = {EPTCS},
    2.15    month = {July},
    2.16 -  note = {To appear, \url{http://eptcs.web.cse.unsw.edu.au/paper.cgi?UITP2014:11}}
    2.17 +  note = {\url{http://eptcs.web.cse.unsw.edu.au/paper.cgi?UITP2014:11}}
    2.18  }
    2.19  
    2.20  @book{principia,