# HG changeset patch # User wenzelm # Date 1381420928 -7200 # Node ID d521407f8d0f350544741c7b2a355e6c2f96c0f5 # Parent 9d156ded3c2af717df0e1c8c121fd89e3b69ec5f more documentation; diff -r 9d156ded3c2a -r d521407f8d0f src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Thu Oct 10 15:46:05 2013 +0200 +++ b/src/Doc/JEdit/JEdit.thy Thu Oct 10 18:02:08 2013 +0200 @@ -306,13 +306,32 @@ the text). Tooltip popups use the same rendering principles as the main text area, and further tooltips and/or hyperlinks may be exposed recursively by the same mechanism. + + %FIXME screenshot of term "x = x" with typing/sorting *} section {* Isabelle symbols and fonts *} -text {* - Isabelle supports infinitely many symbols: +text {* Isabelle sources consist of \emph{symbols} that extend plain + ASCII and UTF-8 (for informal text) to allow infinitely many + mathematical symbols, without depending on particular encodings. + + 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, some well-known symbols are rendered as + Unicode glyphs, in order to show ``@{verbatim "\"}'' as actual + ``@{text "\"}''. This symbol interpretation is specified by the + Isabelle system distribution (in @{file + "$ISABELLE_HOME/etc/symbols"}) or the user (in @{verbatim + "$ISABELLE_HOME_USER/etc/symbols"}). + + \medskip 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. + For example: \medskip \begin{tabular}{l} @@ -324,25 +343,75 @@ \end{tabular} \medskip - A default mapping relates some Isabelle symbols to Unicode points (see - @{file "$ISABELLE_HOME/etc/symbols"} and @{verbatim - "$ISABELLE_HOME_USER/etc/symbols"}. + Correct rendering via Unicode requires a font that contains glyphs + for the corresponding codepoints. Many standard fonts lack that, so + Isabelle/jEdit uses the @{verbatim IsabelleText} by default, which + ensures that standard collection of Isabelle symbols are actually + seen on the screen (or printer). - The \emph{IsabelleText} font ensures that Unicode points are actually seen - on the screen (or printer). + Note that a Java/Swing application can load additional fonts from + the file-system only if they are not installed as system font + already! This means an old version of @{verbatim IsabelleText} that + happens to be already present will prevent Isabelle/jEdit from using + its current bundled version. This might result in missing glyphs + (black rectangles), since @{verbatim IsabelleText} is occasionally + improved in its coverage over time. De-facto there is no need to + ``install'' that font on the system in the first place. + + \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 the latter case, raw @{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 - Input methods: + \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}; jEdit also provides various ways to work with + \emph{abbreviations} to produce certain non-ASCII characters. Since + mathematical characters are far from mainstream use, various + specific Isabelle/jEdit input methods are required. + + Here are some practically relevant input methods for Isabelle + symbols: + \begin{enumerate} - \item use the \emph{Symbols} dockable window - \item copy/paste from decoded source files - \item copy/paste from prover output - \item completion provided by Isabelle plugin, e.g.\ + + \item The \emph{Symbols} panel with some GUI buttoms to insert + certain symbols in the text buffer. There are also tooltips to + reveal to 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 may get re-used to produce further such text. + This also works between different applications, e.g.\ Isabelle/jEdit + and some web browser, as long as the same Unicode view on actual + Isabelle symbols is used. + + \item Copy / paste from prover output within Isabelle/jEdit: the + same principles as for text buffers apply. Note that copy in + Isabelle \emph{Output} works via the keyboard shortcut @{verbatim + "C+v"}, not the jEdit menu (which refers to the main 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 @{verbatim "\"}, or its backslashed name @{verbatim + "\\"}@{verbatim "lambda"}, or its ASCII abbreviation @{verbatim + "%"}. + + The following table is an extract of the information provided by the + standard @{verbatim "etc/symbols"} file: \medskip \begin{tabular}{lll} - \textbf{symbol} & \textbf{abbreviation} & \textbf{backslash escape} \\[1ex] - + \textbf{symbol} & \textbf{abbreviation} & \textbf{backslash escape} \\\hline @{text "\"} & @{verbatim "%"} & @{verbatim "\\lambda"} \\ @{text "\"} & @{verbatim "=>"} & @{verbatim "\\Rightarrow"} \\ @{text "\"} & @{verbatim "==>"} & @{verbatim "\\Longrightarrow"} \\ @@ -363,40 +432,47 @@ \end{enumerate} - \paragraph{Notes:} + Some further notes on symbol completion: + \begin{itemize} \item The above abbreviations refer to the input method. The logical - notation provides ASCII alternatives that often coincide, but deviate - occasionally. + notation provides ASCII alternatives that often coincide, but + deviate occasionally. \item Generic jEdit abbreviations or plugins perform similar source - replacement operations; this works for Isabelle as long as the Unicode - sequences coincide with the symbol mapping. + replacement operations; this works for Isabelle as long as the + Unicode sequences coincide with the symbol mapping. \item Raw Unicode characters within prover source files should be - restricted to informal parts, e.g.\ to write text in non-latin alphabets. - Mathematical symbols should be defined via the official rendering tables. + restricted to informal parts, e.g.\ to write text in non-latin + alphabets. Mathematical symbols should be defined via the official + rendering tables, to avoid problems with portability and longterm + storage of formal text. \end{itemize} - \paragraph{Control symbols.} There are some special control symbols to - modify the style of a \emph{single} symbol (without nesting). Control - symbols may be applied to a region of selected text, either using the - \emph{Symbols} dockable window or keyboard shortcuts. + \paragraph{Control symbols.} There are some special control symbols + to modify the style of a \emph{single} symbol (without + nesting). Control symbols may be applied to a region of selected + text, either using the \emph{Symbols} panel or keyboard shortcuts. \medskip \begin{tabular}{lll} \textbf{symbol} & style & keyboard shortcut \\\hline - @{verbatim "\"} & superscript & @{verbatim "C+e UP"} \\ - @{verbatim "\"} & subscript & @{verbatim "C+e DOWN"} \\ - @{verbatim "\"} & bold face & @{verbatim "C+e RIGHT"} \\ + @{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"} \\ \end{tabular} + + It is also possible to complete on @{verbatim "\\"}@{verbatim sup}, + @{verbatim "\\"}@{verbatim sub}, @{verbatim "\\"}@{verbatim bold} as + for regular symbols. *} -section {* Text completion *} +section {* Text completion \label{sec:completion} *} text {* Text completion works via some light-weight GUI popup, which is triggered by