# HG changeset patch # User wenzelm # Date 1383155229 -3600 # Node ID 7557f9f1d4aafa1f13044bb942a736f230865830 # Parent 5cbe32533cdb31dc95a0a6d0d9c8835572e5da5e misc tuning and clarification; diff -r 5cbe32533cdb -r 7557f9f1d4aa src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Wed Oct 30 17:05:23 2013 +0100 +++ b/src/Doc/JEdit/JEdit.thy Wed Oct 30 18:47:09 2013 +0100 @@ -289,14 +289,14 @@ Moreover note that path specifications in prover input or output usually include formal markup that turns it into a hyperlink (see - also \secref{sec:theory-source}). This allows to open the + also \secref{sec:tooltips-hyperlinks}). This allows to open the corresponding file in the text editor, independently of the path notation. *} chapter {* Prover IDE functionality *} -section {* Text buffers and theories \label{sec:theory-source} *} +section {* Text buffers and theories *} text {* As regular text editor, jEdit maintains a collection of open \emph{text buffers} to store source files; each buffer may be @@ -353,17 +353,22 @@ user to understand the meaning of formal text, and to produce more text with some add-on tools (e.g.\ information messages by automated provers or disprovers running in the background). +*} - Such annotated text can be explored further by using the @{verbatim - CONTROL} modifier key on Linux and Windows, or @{verbatim COMMAND} - on Mac OS X. Hovering with the mouse while the modifier is pressed - reveals a \emph{tooltip} (grey box over the text with a yellow - popup) and/or a \emph{hyperlink} (black rectangle over the text); - see \figref{fig:tooltip}. + +section {* Tooltips and hyperlinks \label{sec:tooltips-hyperlinks} *} + +text {* Formally processed text (prover input or output) contains rich + markup information that can be explored further by using the + @{verbatim CONTROL} modifier key on Linux and Windows, or @{verbatim + COMMAND} on Mac OS X. Hovering with the mouse while the modifier is + pressed reveals a \emph{tooltip} (grey box over the text with a + yellow popup) and/or a \emph{hyperlink} (black rectangle over the + text); see also \figref{fig:tooltip}. \begin{figure}[htbp] \begin{center} - \includegraphics[scale=0.3]{popup1} + \includegraphics[scale=0.6]{popup1} \end{center} \caption{Tooltip and hyperlink for some formal entity.} \label{fig:tooltip} @@ -376,7 +381,7 @@ \begin{figure}[htbp] \begin{center} - \includegraphics[scale=0.3]{popup2} + \includegraphics[scale=0.6]{popup2} \end{center} \caption{Nested tooltips over formal entities.} \label{fig:nested-tooltips} @@ -385,58 +390,80 @@ The tooltip popup window provides some controls to \emph{close} or \emph{detach} the window, turning it into a separate \emph{Info} dockable window managed by jEdit. The @{verbatim ESCAPE} key closes - \emph{all} popups, which is particularly relevant for nested - tooltips stacking up. *} + \emph{all} popups, which is particularly relevant when nested + tooltips are stacking up. + + \medskip A black rectangle in the text indicates a hyperlink that + may be followed by a mouse click (while the @{verbatim CONTROL} or + @{verbatim COMMAND} modifier key is still pressed). Presently (2013) + there is no systematic way to return to the original location within + the editor. + + Also note that the link target may be a file that is itself not + subject to formal document processing of the editor session and thus + prevents further exploration: the chain of hyperlinks may end in + some source file of the underlying logic image, even within the + Isabelle/ML bootstrap sources of Isabelle/Pure, where the formal + markup is less detailed. *} -section {* Isabelle symbols and fonts *} +section {* Isabelle symbols *} text {* Isabelle sources consist of \emph{symbols} that extend plain ASCII to allow infinitely many mathematical symbols within the formal sources. This works without depending on particular - encodings or varying Unicode standards \cite{Wenzel:2011:CICM}. + encodings or varying Unicode standards + \cite{Wenzel:2011:CICM}.\footnote{Raw Unicode characters within + formal sources would compromise portability and reliability in the + face of changing interpretation of various unexpected features of + Unicode.} For the prover back-end, formal text consists of ASCII characters that are grouped according to some simple rules, e.g.\ as plain ``@{verbatim a}'' or symbolic ``@{verbatim "\"}''. - For the editor front-end, a certain subset of symbols is rendered as - Unicode glyphs, in order to show ``@{verbatim "\"}'' as ``@{text - "\"}'', for example. This symbol interpretation is specified by the - Isabelle system distribution (@{file "$ISABELLE_HOME/etc/symbols"}) - or by the user (@{verbatim "$ISABELLE_HOME_USER/etc/symbols"}). + For the editor front-end, a certain subset of symbols is rendered + physically via Unicode glyphs, in order to show ``@{verbatim "\"}'' + as ``@{text "\"}'', 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 + @{verbatim "$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 - collection. Uninterpreted symbols are shown literally, e.g.\ - ``@{verbatim "\"}''. + collection. Uninterpreted symbols are displayed literally, e.g.\ + ``@{verbatim "\"}''. Overlap of Unicode characters used in + symbol interpretation with informal ones that might appear e.g.\ in + comments needs to be avoided! - \medskip Technically, the Unicode view on Isabelle symbols is an - \emph{encoding} in Isabelle/jEdit, which is called @{verbatim - "UTF-8-Isabelle"} and enabled by default. Sometimes such defaults - are reset accidentally, or malformed UTF-8 sequences in the text - force jEdit to fall back on a different encoding like @{verbatim - "ISO-8859-15"}. In that case, verbatim ``@{verbatim "\"}'' will be - shown in the text buffer instead of its Unicode rendering ``@{text - "\"}''. The jEdit menu operation \emph{File / Reload with Encoding - / UTF-8-Isabelle} helps to resolve such problems, potentially after - repairing malformed parts of the text. + \medskip \paragraph{Encoding.} Technically, the Unicode view on + Isabelle symbols is an \emph{encoding} in jEdit (not in the + underlying JVM) that is called @{verbatim "UTF-8-Isabelle"}. It is + provided by the Isabelle/jEdit plugin and enabled by default for all + source files. Sometimes such defaults are reset accidentally, or + malformed UTF-8 sequences in the text force jEdit to fall back on a + different encoding like @{verbatim "ISO-8859-15"}. In that case, + verbatim ``@{verbatim "\"}'' will be shown in the text buffer + instead of its Unicode rendering ``@{text "\"}''. The jEdit menu + operation \emph{File / Reload with Encoding / UTF-8-Isabelle} helps + to resolve such problems, potentially after repairing malformed + parts of the text. - \medskip Correct rendering via Unicode requires a font that contains - glyphs for the corresponding codepoints. Most system fonts lack - that, so Isabelle/jEdit prefers its own application font @{verbatim - IsabelleText}, which ensures that standard collection of Isabelle - symbols are actually seen on the screen (or printer). + \medskip \paragraph{Font.} Correct rendering via Unicode requires a + font that contains glyphs for the corresponding codepoints. Most + system fonts lack that, so Isabelle/jEdit prefers its own + application font @{verbatim IsabelleText}, which ensures that + standard collection of Isabelle symbols are actually seen on the + screen (or printer). Note that a Java/AWT/Swing application can load additional fonts only if they are not installed as system font already! This means some old version of @{verbatim IsabelleText} that happens to be already present prevents Isabelle/jEdit from using its current - bundled version. This might result in missing glyphs (black - rectangles), since obsolete versions of @{verbatim IsabelleText} - lack recent improvements of Unicode glyph coverage. This problem - can be avoided by refraining to ``install'' any version of - @{verbatim IsabelleText} in the first place. + bundled version. This results in missing glyphs (black rectangles), + when some obsolete version of @{verbatim IsabelleText} is used by + accident. This problem can be avoided by refraining to ``install'' + any version of @{verbatim IsabelleText} in the first place. \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit could delegate the problem to produce Isabelle symbols in their @@ -458,15 +485,16 @@ information about \emph{symbol abbreviations} (see below). \item Copy / paste from decoded source files: text that is rendered - as Unicode already can be re-used to produce further such text. - This also works between different applications, e.g.\ Isabelle/jEdit - and some web browser or mail client, as long as the same Unicode - view on Isabelle symbols is used uniformly. + as Unicode already can be re-used to produce further text. This + also works between different applications, e.g.\ Isabelle/jEdit and + some web browser or mail client, as long as the same Unicode view on + Isabelle symbols is used uniformly. \item Copy / paste from prover output within Isabelle/jEdit. The same principles as for text buffers apply, but note that \emph{copy} - in Isabelle \emph{Output} works via the keyboard shortcut @{verbatim - "C+c"}, not jEdit menu actions. + in secondary Isabelle/jEdit windows works via the keyboard shortcut + @{verbatim "C+c"}. The jEdit menu actions always refer to the + primary text area! \item Completion provided by Isabelle plugin (see \secref{sec:completion}). Isabelle symbols have a canonical name @@ -503,9 +531,9 @@ Note that the above abbreviations refer to the input method. The logical notation provides ASCII alternatives that often coincide, - but deviate occasionally. Writing formal sources directly with - ASCII replacement notation like @{verbatim "!"} or @{verbatim "ALL"} - is considered old-fashioned in 2013! + but deviate occasionally. This occasionally causes user confusion + with very old-fashioned Isabelle source that use ASCII replacement + notation like @{verbatim "!"} or @{verbatim "ALL"} directly. \end{enumerate} @@ -518,23 +546,24 @@ \paragraph{Control symbols.} There are some special control symbols to modify the style of a single symbol (without nesting). Control symbols may be applied to a region of selected text, either using - the \emph{Symbols} panel or keyboard shortcuts; these editor - operations produce a separate control symbol for each symbol in the - text, in order to make the whole text appear in a certain style. + the \emph{Symbols} panel or keyboard shortcuts or jEdit actions. + These editor operations produce a separate control symbol for each + symbol in the text, in order to make the whole text appear in a + certain style. \medskip - \begin{tabular}{lll} - \textbf{symbol} & style & keyboard shortcut \\\hline - @{verbatim "\<^sup>"} & superscript & @{verbatim "C+e UP"} \\ - @{verbatim "\<^sub>"} & subscript & @{verbatim "C+e DOWN"} \\ - @{verbatim "\<^bold>"} & bold face & @{verbatim "C+e RIGHT"} \\ - & reset & @{verbatim "C+e LEFT"} \\ + \begin{tabular}{llll} + style & \textbf{symbol} & shortcut & action \\\hline + superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{verbatim "isabelle.control-sup"} \\ + subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{verbatim "isabelle.control-sub"} \\ + bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{verbatim "isabelle.control-bold"} \\ + reset & & @{verbatim "C+e LEFT"} & @{verbatim "isabelle.control-reset"} \\ \end{tabular} + \medskip - It is also possible to complete on @{verbatim "\\"}@{verbatim sup}, - @{verbatim "\\"}@{verbatim sub}, @{verbatim "\\"}@{verbatim bold} as - for regular symbols. -*} + To produce a single control symbol, it is also possible to complete + on @{verbatim "\\"}@{verbatim sup}, @{verbatim "\\"}@{verbatim sub}, + @{verbatim "\\"}@{verbatim bold} as for regular symbols. *} section {* Text completion \label{sec:completion} *}