# HG changeset patch # User wenzelm # Date 1402336558 -7200 # Node ID 3ca8216f4a96b2f27bb129a2d02ed427d1981148 # Parent 2b89a3a34cc3f2e52e3e06e67840599157961caa clarified section structure; diff -r 2b89a3a34cc3 -r 3ca8216f4a96 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Mon Jun 09 19:43:54 2014 +0200 +++ b/src/Doc/JEdit/JEdit.thy Mon Jun 09 19:55:58 2014 +0200 @@ -317,6 +317,211 @@ *} +section {* Isabelle symbols \label{sec: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 and 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 special features of Unicode, such + as Combining Characters or Bi-directional Text.} + + 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 + 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 + @{file_unchecked "$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 displayed literally, e.g.\ + ``@{verbatim "\"}''. Overlap of Unicode characters used in + symbol interpretation with informal ones (which might appear e.g.\ + in comments) needs to be avoided! Raw Unicode characters within + prover source files should be restricted to informal parts, e.g.\ to + write text in non-latin alphabets in comments. + + \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 \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 on the operating system already! + Some old version of @{verbatim IsabelleText} that happens to be + provided by the operating system would prevent Isabelle/jEdit to use + its bundled version. This could lead to missing glyphs (black + rectangles), when the system version of @{verbatim IsabelleText} is + older than the application version. This problem can be avoided by + refraining to ``install'' any version of @{verbatim IsabelleText} in + the first place (although it is occasionally tempting to use + the same font in other applications). + + \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit + could delegate the problem to produce Isabelle symbols in their + Unicode rendering to the underlying operating system and its + \emph{input methods}. Regular jEdit also provides various ways to + work with \emph{abbreviations} to produce certain non-ASCII + characters. Since none of these standard input methods work + satisfactorily for the mathematical characters required for + Isabelle, various specific Isabelle/jEdit mechanisms are provided. + + Here is a summary for practically relevant input methods for + Isabelle symbols: + + \begin{enumerate} + + \item The \emph{Symbols} panel: some GUI buttons allow to insert + certain symbols in the text buffer. There are also tooltips to + reveal the official Isabelle representation with some additional + 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 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. + + \item Copy / paste from prover output within Isabelle/jEdit. The + same principles as for text buffers apply, but note that \emph{copy} + in secondary Isabelle/jEdit windows works via the keyboard shortcut + @{verbatim "C+c"}, while 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 + and optional abbreviations. This can be used with the text + completion mechanism of Isabelle/jEdit, to replace a prefix of the + actual symbol like @{verbatim "\"}, or its backslashed name + @{verbatim "\\"}@{verbatim "lambda"}, or its ASCII abbreviation + @{verbatim "%"} by the Unicode rendering. + + The following table is an extract of the information provided by the + standard @{file "$ISABELLE_HOME/etc/symbols"} file: + + \medskip + \begin{tabular}{lll} + \textbf{symbol} & \textbf{backslashed name} & \textbf{abbreviation} \\\hline + @{text "\"} & @{verbatim "\\lambda"} & @{verbatim "%"} \\ + @{text "\"} & @{verbatim "\\Rightarrow"} & @{verbatim "=>"} \\ + @{text "\"} & @{verbatim "\\Longrightarrow"} & @{verbatim "==>"} \\[0.5ex] + @{text "\"} & @{verbatim "\\And"} & @{verbatim "!!"} \\ + @{text "\"} & @{verbatim "\\equiv"} & @{verbatim "=="} \\[0.5ex] + @{text "\"} & @{verbatim "\\forall"} & @{verbatim "!"} \\ + @{text "\"} & @{verbatim "\\exists"} & @{verbatim "?"} \\ + @{text "\"} & @{verbatim "\\longrightarrow"} & @{verbatim "-->"} \\ + @{text "\"} & @{verbatim "\\and"} & @{verbatim "&"} \\ + @{text "\"} & @{verbatim "\\or"} & @{verbatim "|"} \\ + @{text "\"} & @{verbatim "\\not"} & @{verbatim "~"} \\ + @{text "\"} & @{verbatim "\\noteq"} & @{verbatim "~="} \\ + @{text "\"} & @{verbatim "\\in"} & @{verbatim ":"} \\ + @{text "\"} & @{verbatim "\\notin"} & @{verbatim "~:"} \\ + \end{tabular} + \medskip + + Note that the above abbreviations refer to the input method. The + logical notation provides ASCII alternatives that often coincide, + 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 in the + text. + + On the other hand, coincidence of symbol abbreviations with ASCII + replacement syntax syntax helps to update old theory sources via + explicit completion (see also @{verbatim "C+b"} explained in + \secref{sec:completion}). + + \end{enumerate} + + \paragraph{Control symbols.} There are some special control symbols + to modify the display 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 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}{llll} + \textbf{style} & \textbf{symbol} & \textbf{shortcut} & \textbf{action} \\\hline + superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{action "isabelle.control-sup"} \\ + subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{action "isabelle.control-sub"} \\ + bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{action "isabelle.control-bold"} \\ + reset & & @{verbatim "C+e LEFT"} & @{action "isabelle.control-reset"} \\ + \end{tabular} + \medskip + + 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 {* SideKick parsers \label{sec:sidekick} *} + +text {* + The \emph{SideKick} plugin provides some general services to display buffer + structure in a tree view. + + Isabelle/jEdit provides SideKick parsers for its main mode for + theory files, as well as some minor modes for the @{verbatim NEWS} + file, session @{verbatim ROOT} files, and system @{verbatim + options}. + + Moreover, the special SideKick parser @{verbatim "isabelle-markup"} + provides access to the full (uninterpreted) markup tree of the PIDE + document model of the current buffer. This is occasionally useful + for informative purposes, but the amount of displayed information + might cause problems for large buffers, both for the human and the + machine. +*} + + +section {* Scala console \label{sec:scala-console} *} + +text {* + The \emph{Console} plugin manages various shells (command interpreters), + e.g.\ \emph{BeanShell}, which is the official jEdit scripting language, and + the cross-platform \emph{System} shell. Thus the console provides similar + functionality than the special Emacs buffers @{verbatim "*scratch*"} and + @{verbatim "*shell*"}. + + Isabelle/jEdit extends the repertoire of the console by \emph{Scala}, which + is the regular Scala toplevel loop running inside the \emph{same} JVM + process as Isabelle/jEdit itself. This means the Scala command interpreter + has access to the JVM name space and state of the running Prover IDE + application: the main entry points are @{verbatim view} (the current editor + view of jEdit) and @{verbatim PIDE} (the Isabelle/jEdit plugin object). For + example, the Scala expression @{verbatim "PIDE.snapshot(view)"} makes a PIDE + document snapshot of the current buffer within the current editor view. + + This helps to explore Isabelle/Scala functionality interactively. Some care + is required to avoid interference with the internals of the running + application, especially in production use. +*} + + section {* File-system access *} text {* File specifications in jEdit follow various formats and @@ -370,50 +575,6 @@ *} -section {* SideKick parsers \label{sec:sidekick} *} - -text {* - The \emph{SideKick} plugin provides some general services to display buffer - structure in a tree view. - - Isabelle/jEdit provides SideKick parsers for its main mode for - theory files, as well as some minor modes for the @{verbatim NEWS} - file, session @{verbatim ROOT} files, and system @{verbatim - options}. - - Moreover, the special SideKick parser @{verbatim "isabelle-markup"} - provides access to the full (uninterpreted) markup tree of the PIDE - document model of the current buffer. This is occasionally useful - for informative purposes, but the amount of displayed information - might cause problems for large buffers, both for the human and the - machine. -*} - - -section {* Scala console \label{sec:scala-console} *} - -text {* - The \emph{Console} plugin manages various shells (command interpreters), - e.g.\ \emph{BeanShell}, which is the official jEdit scripting language, and - the cross-platform \emph{System} shell. Thus the console provides similar - functionality than the special Emacs buffers @{verbatim "*scratch*"} and - @{verbatim "*shell*"}. - - Isabelle/jEdit extends the repertoire of the console by \emph{Scala}, which - is the regular Scala toplevel loop running inside the \emph{same} JVM - process as Isabelle/jEdit itself. This means the Scala command interpreter - has access to the JVM name space and state of the running Prover IDE - application: the main entry points are @{verbatim view} (the current editor - view of jEdit) and @{verbatim PIDE} (the Isabelle/jEdit plugin object). For - example, the Scala expression @{verbatim "PIDE.snapshot(view)"} makes a PIDE - document snapshot of the current buffer within the current editor view. - - This helps to explore Isabelle/Scala functionality interactively. Some care - is required to avoid interference with the internals of the running - application, especially in production use. -*} - - chapter {* Prover IDE functionality *} section {* Text buffers and theories \label{sec:buffers-theories} *} @@ -793,167 +954,6 @@ @{verbatim undo} operation of jEdit. *} -section {* Isabelle symbols \label{sec: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 and 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 special features of Unicode, such - as Combining Characters or Bi-directional Text.} - - 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 - 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 - @{file_unchecked "$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 displayed literally, e.g.\ - ``@{verbatim "\"}''. Overlap of Unicode characters used in - symbol interpretation with informal ones (which might appear e.g.\ - in comments) needs to be avoided! Raw Unicode characters within - prover source files should be restricted to informal parts, e.g.\ to - write text in non-latin alphabets in comments. - - \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 \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 on the operating system already! - Some old version of @{verbatim IsabelleText} that happens to be - provided by the operating system would prevent Isabelle/jEdit to use - its bundled version. This could lead to missing glyphs (black - rectangles), when the system version of @{verbatim IsabelleText} is - older than the application version. This problem can be avoided by - refraining to ``install'' any version of @{verbatim IsabelleText} in - the first place (although it is occasionally tempting to use - the same font in other applications). - - \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit - could delegate the problem to produce Isabelle symbols in their - Unicode rendering to the underlying operating system and its - \emph{input methods}. Regular jEdit also provides various ways to - work with \emph{abbreviations} to produce certain non-ASCII - characters. Since none of these standard input methods work - satisfactorily for the mathematical characters required for - Isabelle, various specific Isabelle/jEdit mechanisms are provided. - - Here is a summary for practically relevant input methods for - Isabelle symbols: - - \begin{enumerate} - - \item The \emph{Symbols} panel: some GUI buttons allow to insert - certain symbols in the text buffer. There are also tooltips to - reveal the official Isabelle representation with some additional - 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 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. - - \item Copy / paste from prover output within Isabelle/jEdit. The - same principles as for text buffers apply, but note that \emph{copy} - in secondary Isabelle/jEdit windows works via the keyboard shortcut - @{verbatim "C+c"}, while 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 - and optional abbreviations. This can be used with the text - completion mechanism of Isabelle/jEdit, to replace a prefix of the - actual symbol like @{verbatim "\"}, or its backslashed name - @{verbatim "\\"}@{verbatim "lambda"}, or its ASCII abbreviation - @{verbatim "%"} by the Unicode rendering. - - The following table is an extract of the information provided by the - standard @{file "$ISABELLE_HOME/etc/symbols"} file: - - \medskip - \begin{tabular}{lll} - \textbf{symbol} & \textbf{backslashed name} & \textbf{abbreviation} \\\hline - @{text "\"} & @{verbatim "\\lambda"} & @{verbatim "%"} \\ - @{text "\"} & @{verbatim "\\Rightarrow"} & @{verbatim "=>"} \\ - @{text "\"} & @{verbatim "\\Longrightarrow"} & @{verbatim "==>"} \\[0.5ex] - @{text "\"} & @{verbatim "\\And"} & @{verbatim "!!"} \\ - @{text "\"} & @{verbatim "\\equiv"} & @{verbatim "=="} \\[0.5ex] - @{text "\"} & @{verbatim "\\forall"} & @{verbatim "!"} \\ - @{text "\"} & @{verbatim "\\exists"} & @{verbatim "?"} \\ - @{text "\"} & @{verbatim "\\longrightarrow"} & @{verbatim "-->"} \\ - @{text "\"} & @{verbatim "\\and"} & @{verbatim "&"} \\ - @{text "\"} & @{verbatim "\\or"} & @{verbatim "|"} \\ - @{text "\"} & @{verbatim "\\not"} & @{verbatim "~"} \\ - @{text "\"} & @{verbatim "\\noteq"} & @{verbatim "~="} \\ - @{text "\"} & @{verbatim "\\in"} & @{verbatim ":"} \\ - @{text "\"} & @{verbatim "\\notin"} & @{verbatim "~:"} \\ - \end{tabular} - \medskip - - Note that the above abbreviations refer to the input method. The - logical notation provides ASCII alternatives that often coincide, - 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 in the - text. - - On the other hand, coincidence of symbol abbreviations with ASCII - replacement syntax syntax helps to update old theory sources via - explicit completion (see also @{verbatim "C+b"} explained in - \secref{sec:completion}). - - \end{enumerate} - - \paragraph{Control symbols.} There are some special control symbols - to modify the display 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 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}{llll} - \textbf{style} & \textbf{symbol} & \textbf{shortcut} & \textbf{action} \\\hline - superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{action "isabelle.control-sup"} \\ - subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{action "isabelle.control-sub"} \\ - bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{action "isabelle.control-bold"} \\ - reset & & @{verbatim "C+e LEFT"} & @{action "isabelle.control-reset"} \\ - \end{tabular} - \medskip - - 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 {* Automatically tried tools \label{sec:auto-tools} *} text {* Continuous document processing works asynchronously in the