1.1 --- a/src/Doc/JEdit/JEdit.thy	Thu Oct 10 14:29:21 2013 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu Oct 10 15:46:05 2013 +0200
     1.3 @@ -195,7 +195,7 @@
     1.4  *}
     1.5  
     1.6  
     1.7 -section {* Platform look-and-feel *}
     1.8 +subsection {* Look-and-feel *}
     1.9  
    1.10  text {* jEdit is a Java/Swing application with some ambition to
    1.11    support ``native'' platform look-and-feel, within the limits of what
    1.12 @@ -207,11 +207,9 @@
    1.13    \begin{description}
    1.14  
    1.15    \item[Linux] The platform-independent \emph{Nimbus} is used by
    1.16 -  default, but the classic \emph{Metal} also works.
    1.17 -
    1.18 -  Quasi-native \emph{GTK+} works under the side-condition that the
    1.19 -  overall GTK theme is selected in a Java/Swing friendly way: the
    1.20 -  success rate is @{text "\<approx>"} 50\%.
    1.21 +  default, but the classic \emph{Metal} also works.  \emph{GTK+} works
    1.22 +  under the side-condition that the overall GTK theme is selected in a
    1.23 +  Java/Swing friendly way: the success rate is @{text "\<approx>"} 50\%.
    1.24  
    1.25    \item[Windows] Regular \emph{Windows} is used by default, but
    1.26    platform-independent \emph{Nimbus} and \emph{Metal} also work.
    1.27 @@ -240,30 +238,75 @@
    1.28  
    1.29  chapter {* Prover IDE functionality *}
    1.30  
    1.31 -section {* Main text area *}
    1.32 +section {* Buffers and theories *}
    1.33  
    1.34 -text {*
    1.35 +text {* jEdit maintains a collection of open \emph{text buffers} to
    1.36 +  store source files.  Each buffer may be associated with any number
    1.37 +  of \emph{text areas} as visible GUI representation of the content.
    1.38  
    1.39 -  Source files with \texttt{.thy} extension are treated specifically:
    1.40 -  Isabelle/jEdit adds them to the formal document-model of Isabelle/PIDE, that
    1.41 -  maintains semantic information provided by the prover in the background,
    1.42 -  while the user is editing the text in the foreground.
    1.43 +  Buffers are subject to a \emph{mode} that is determined from the
    1.44 +  file type.  Files with extension \texttt{.thy} are assigned to the
    1.45 +  mode \emph{isabelle} and treated specifically as follows.
    1.46  
    1.47 -  \medskip Physical rendering of document content draws from the
    1.48 -  standard repertoire of known IDEs for programming languages, with
    1.49 -  highlighting, squiggles, tooltips, hyperlinks etc.  In the above
    1.50 -  screenshot, only the bold keywords of the Isar language use
    1.51 -  traditional syntax-highlighting in jEdit with static tables; all
    1.52 -  other coloring is based on dynamic information from the logical
    1.53 -  context of the prover.
    1.54 +  \begin{itemize}
    1.55  
    1.56 -  Such annotated text regions can be explored further by using the
    1.57 -  \texttt{CONTROL} modifier key (or \texttt{COMMAND} on Mac OS X),
    1.58 -  together with mouse hovering or clicking.  It reveals tooltips and
    1.59 -  hyperlinks, e.g.\ see \texttt{constant "Example.path"} above, and
    1.60 -  thus explains how a certain piece of source text has been
    1.61 -  interpreted.
    1.62 - *}
    1.63 +  \item Theory files are implicitly added to the formal document model
    1.64 +  of Isabelle/jEdit, which maintains a family of versions of all
    1.65 +  sources for the prover in the background.  The \emph{Theories} panel
    1.66 +  provides an overview of the status of continuous checking of theory
    1.67 +  sources.  Unlike batch sessions \cite{isabelle-sys}, full theory
    1.68 +  file names are used to identify theory nodes; this allows to
    1.69 +  experiment with multiple (disjoint) Isabelle sessions
    1.70 +  simultaneously.
    1.71 +
    1.72 +  \item Certain events to open or update buffers containing theory
    1.73 +  files cause Isabelle/jEdit to resolve dependencies of \emph{theory
    1.74 +  imports}.  The system will request to load further files into jEdit
    1.75 +  editor buffers, which will eventually be added to the theory
    1.76 +  document model for further checking.  It is also possible to resolve
    1.77 +  dependencies automatically, depending on the option @{system_option
    1.78 +  jedit_auto_load}.
    1.79 +
    1.80 +  \item Physical rendering of jEdit buffer content within the visible
    1.81 +  text areas is augmented by information from the formal document
    1.82 +  model.  Thus the prover can provide additional markup to help the
    1.83 +  user understanding the meaning of the text, and to produce more text
    1.84 +  with some add-on tools (e.g.\ information messages produced by
    1.85 +  automated provers or disprovers in the background).
    1.86 +
    1.87 +  \end{itemize}
    1.88 +
    1.89 +  The text area views on theory buffers define the visible part of the
    1.90 +  \emph{perspective} of Isabelle/jEdit.  This is taken as a hint for
    1.91 +  document processing: the prover will ensure that those parts of a
    1.92 +  theory where the user is looking are checked, while invisible parts
    1.93 +  that are presently not required are left alone.
    1.94 +
    1.95 +  The perspective can may changed by opening or closing text areas, or
    1.96 +  scrolling the corresponding windows.  It is also possible to
    1.97 +  indicate theory nodes as \emph{required} for continuous checking in
    1.98 +  the \emph{Theories} panel.  This means such nodes and all their
    1.99 +  imports are always processed, independently of the visibility
   1.100 +  status.  This can have significant impact on performance, though.
   1.101 +
   1.102 +  \medskip Formal markup of checked theory content is turned into GUI
   1.103 +  rendering, based on a standard repertoire known from IDEs for
   1.104 +  programming languages: colors, icons, highlighting, squiggly
   1.105 +  underline, tooltips, hyperlinks etc.  There is some traditional
   1.106 +  syntax-highlighting for the outer syntax of Isabelle/Isar, based on
   1.107 +  static keyword tables.  The coloring of inner syntax (term language
   1.108 +  etc.) is based on dynamic information from the logical context of
   1.109 +  the prover.
   1.110 +
   1.111 +  Such formally annotated text can be explored further by using the
   1.112 +  @{verbatim CONTROL} modifier key on Linux or Windows, and @{verbatim
   1.113 +  COMMAND} on Mac OS X.  Hovering with the mouse while the modifier is
   1.114 +  pressed reveals \emph{tooltips} (grey box within the text with a
   1.115 +  yellow popup) and/or \emph{hyperlinks} (dark grey rectangle within
   1.116 +  the text).  Tooltip popups use the same rendering principles as the
   1.117 +  main text area, and further tooltips and/or hyperlinks may be
   1.118 +  exposed recursively by the same mechanism.
   1.119 +*}
   1.120  
   1.121  
   1.122  section {* Isabelle symbols and fonts *}