1.1 --- a/src/Doc/JEdit/JEdit.thy Tue Oct 29 19:45:55 2013 +0100
1.2 +++ b/src/Doc/JEdit/JEdit.thy Tue Oct 29 21:00:37 2013 +0100
1.3 @@ -247,14 +247,14 @@
1.4
1.5 chapter {* Prover IDE functionality *}
1.6
1.7 -section {* Buffers and theories *}
1.8 +section {* Text buffers and theories *}
1.9
1.10 -text {* jEdit maintains a collection of open \emph{text buffers} to
1.11 - store source files. Each buffer may be associated with any number
1.12 - of visible \emph{text areas}. Buffers are subject to an \emph{edit
1.13 - mode} that is determined from the file type. Files with extension
1.14 - \texttt{.thy} are assigned to the mode \emph{isabelle} and treated
1.15 - specifically.
1.16 +text {* As regular text editor, jEdit maintains a collection of open
1.17 + \emph{text buffers} to store source files; each buffer may be
1.18 + associated with any number of visible \emph{text areas}. Buffers
1.19 + are subject to an \emph{edit mode} that is determined from the file
1.20 + type. Files with extension \texttt{.thy} are assigned to the mode
1.21 + \emph{isabelle} and treated specifically.
1.22
1.23 \medskip Isabelle theory files are automatically added to the formal
1.24 document model of Isabelle/Scala, which maintains a family of
1.25 @@ -267,23 +267,25 @@
1.26
1.27 Certain events to open or update buffers with theory files cause
1.28 Isabelle/jEdit to resolve dependencies of \emph{theory imports}.
1.29 - The system requests to load further files into editor buffers, in
1.30 - order to be added to the theory document model for further checking.
1.31 - It is also possible to resolve dependencies automatically, depending
1.32 - on the option @{system_option jedit_auto_load}.
1.33 + The system requests to load additional files into editor buffers, in
1.34 + order to be included in the theory document model for further
1.35 + checking. It is also possible to resolve dependencies
1.36 + automatically, depending on \emph{Plugin Options / Isabelle /
1.37 + General / Auto load} (Isabelle system option @{system_option
1.38 + jedit_auto_load}).
1.39
1.40 \medskip The open text area views on theory buffers define the
1.41 visible \emph{perspective} of Isabelle/jEdit. This is taken as a
1.42 hint for document processing: the prover ensures that those parts of
1.43 a theory where the user is looking are checked, while other parts
1.44 - that are presently not required are ignored. The perspective can be
1.45 + that are presently not required are ignored. The perspective is
1.46 changed by opening or closing text area windows, or scrolling within
1.47 some window.
1.48
1.49 The \emph{Theories} panel provides some further options to influence
1.50 the process of continuous checking: it may be switched off globally
1.51 - to perform superficial processing of command syntax only. It is
1.52 - also possible to indicate theory nodes as \emph{required} for
1.53 + to restrict the prover to superficial processing of command syntax.
1.54 + It is also possible to indicate theory nodes as \emph{required} for
1.55 continuous checking: this means such nodes and all their imports are
1.56 always processed independently of the visibility status (if
1.57 continuous checking is enabled). Big theory libraries that are
1.58 @@ -294,40 +296,48 @@
1.59 rendering, based on a standard repertoire known from IDEs for
1.60 programming languages: colors, icons, highlighting, squiggly
1.61 underline, tooltips, hyperlinks etc. For outer syntax of
1.62 - Isabelle/Isar there is some traditional syntax-highlighting, based
1.63 - on static keyword tables and tokenization within the editor. In
1.64 - contrast, the painting of inner syntax (term language etc.) is
1.65 - based on semantic information that is reported dynamically from the
1.66 - logical context. Thus the prover can provide additional markup to
1.67 - help the user understanding the meaning of the text, and to produce
1.68 - more text with some add-on tools (e.g.\ information messages by
1.69 - automated provers or disprovers running in the background).
1.70 + Isabelle/Isar there is some traditional syntax-highlighting via
1.71 + static keyword tables and tokenization within the editor. In
1.72 + contrast, the painting of inner syntax (term language etc.)\ uses
1.73 + semantic information that is reported dynamically from the logical
1.74 + context. Thus the prover can provide additional markup to help the
1.75 + user to understand the meaning of formal text, and to produce more
1.76 + text with some add-on tools (e.g.\ information messages by automated
1.77 + provers or disprovers running in the background).
1.78
1.79 - Such formally annotated text can be explored further by using the
1.80 - @{verbatim CONTROL} modifier key on Linux and Windows, or @{verbatim
1.81 - COMMAND} on Mac OS X. Hovering with the mouse while the modifier is
1.82 - pressed reveals \emph{tooltips} (grey box within the text with a
1.83 - yellow popup) and/or \emph{hyperlinks} (dark grey rectangle within
1.84 - the text).
1.85 + Such annotated text can be explored further by using the @{verbatim
1.86 + CONTROL} modifier key on Linux and Windows, or @{verbatim COMMAND}
1.87 + on Mac OS X. Hovering with the mouse while the modifier is pressed
1.88 + reveals a \emph{tooltip} (grey box over the text with a yellow
1.89 + popup) and/or a \emph{hyperlink} (black rectangle over the text);
1.90 + see \figref{fig:tooltip}.
1.91
1.92 \begin{figure}[htbp]
1.93 \begin{center}
1.94 \includegraphics[scale=0.3]{popup1}
1.95 \end{center}
1.96 - \caption{Hyperlink and tooltip for some formal entity.}
1.97 + \caption{Tooltip and hyperlink for some formal entity.}
1.98 + \label{fig:tooltip}
1.99 \end{figure}
1.100
1.101 - Tooltip popups use the same rendering principles as the
1.102 - main text area, and further tooltips and/or hyperlinks may be
1.103 - exposed recursively by the same mechanism.
1.104 + Tooltip popups use the same rendering principles as the main text
1.105 + area, and further tooltips and/or hyperlinks may be exposed
1.106 + recursively by the same mechanism; see
1.107 + \figref{fig:nested-tooltips}.
1.108
1.109 \begin{figure}[htbp]
1.110 \begin{center}
1.111 \includegraphics[scale=0.3]{popup2}
1.112 \end{center}
1.113 \caption{Nested tooltips over formal entities.}
1.114 + \label{fig:nested-tooltips}
1.115 \end{figure}
1.116 -*}
1.117 +
1.118 + The tooltip popup window provides some controls to \emph{close} or
1.119 + \emph{detach} the window, turning it into a separate \emph{Info}
1.120 + dockable window managed by jEdit. The @{verbatim ESCAPE} key closes
1.121 + \emph{all} popups, which is particularly relevant for nested
1.122 + tooltips stacking up. *}
1.123
1.124
1.125 section {* Isabelle symbols and fonts *}