--- a/src/Doc/Implementation/ML.thy Thu Oct 22 21:16:49 2015 +0200
+++ b/src/Doc/Implementation/ML.thy Thu Oct 22 21:34:28 2015 +0200
@@ -1213,35 +1213,32 @@
section \<open>Strings of symbols \label{sec:symbols}\<close>
-text \<open>A \<^emph>\<open>symbol\<close> constitutes the smallest textual unit in
- Isabelle/ML --- raw ML characters are normally not encountered at
- all. Isabelle strings consist of a sequence of symbols, represented
- as a packed string or an exploded list of strings. Each symbol is
- in itself a small string, which has either one of the following
- forms:
-
- \<^enum> a single ASCII character ``\<open>c\<close>'', for example ``\<^verbatim>\<open>a\<close>'',
-
- \<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence),
-
- \<^enum> a regular symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close>'', for example ``\<^verbatim>\<open>\<alpha>\<close>'',
-
- \<^enum> a control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close>'', for example ``\<^verbatim>\<open>\<^bold>\<close>'',
-
- \<^enum> a raw symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw:\<close>\<open>text\<close>\<^verbatim>\<open>>\<close>'' where \<open>text\<close> consists of printable characters
- excluding ``\<^verbatim>\<open>.\<close>'' and ``\<^verbatim>\<open>>\<close>'', for example
- ``\<^verbatim>\<open>\<^raw:$\sum_{i = 1}^n$>\<close>'',
-
- \<^enum> a numbered raw control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw\<close>\<open>n\<close>\<^verbatim>\<open>>\<close>, where \<open>n\<close> consists
- of digits, for example ``\<^verbatim>\<open>\<^raw42>\<close>''.
-
-
- The \<open>ident\<close> syntax for symbol names is \<open>letter
- (letter | digit)\<^sup>*\<close>, where \<open>letter = A..Za..z\<close> and \<open>digit = 0..9\<close>. There are infinitely many regular symbols and
- control symbols, but a fixed collection of standard symbols is
- treated specifically. For example, ``\<^verbatim>\<open>\<alpha>\<close>'' is
- classified as a letter, which means it may occur within regular
- Isabelle identifiers.
+text \<open>A \<^emph>\<open>symbol\<close> constitutes the smallest textual unit in Isabelle/ML --- raw
+ ML characters are normally not encountered at all. Isabelle strings consist
+ of a sequence of symbols, represented as a packed string or an exploded list
+ of strings. Each symbol is in itself a small string, which has either one of
+ the following forms:
+
+ \<^enum> a single ASCII character ``\<open>c\<close>'', for example ``\<^verbatim>\<open>a\<close>'',
+
+ \<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence),
+
+ \<^enum> a regular symbol ``\<^verbatim>\<open>\<ident>\<close>'', for example ``\<^verbatim>\<open>\<alpha>\<close>'',
+
+ \<^enum> a control symbol ``\<^verbatim>\<open>\<^ident>\<close>'', for example ``\<^verbatim>\<open>\<^bold>\<close>'',
+
+ \<^enum> a raw symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw:\<close>\<open>text\<close>\<^verbatim>\<open>>\<close>'' where \<open>text\<close> consists of
+ printable characters excluding ``\<^verbatim>\<open>.\<close>'' and ``\<^verbatim>\<open>>\<close>'', for example
+ ``\<^verbatim>\<open>\<^raw:$\sum_{i = 1}^n$>\<close>'',
+
+ \<^enum> a numbered raw control symbol ``\<^verbatim>\<open>\\<close>\<^verbatim>\<open><^raw\<close>\<open>n\<close>\<^verbatim>\<open>>\<close>, where \<open>n\<close> consists
+ of digits, for example ``\<^verbatim>\<open>\<^raw42>\<close>''.
+
+ The \<open>ident\<close> syntax for symbol names is \<open>letter (letter | digit)\<^sup>*\<close>, where
+ \<open>letter = A..Za..z\<close> and \<open>digit = 0..9\<close>. There are infinitely many regular
+ symbols and control symbols, but a fixed collection of standard symbols is
+ treated specifically. For example, ``\<^verbatim>\<open>\<alpha>\<close>'' is classified as a letter, which
+ means it may occur within regular Isabelle identifiers.
The character set underlying Isabelle symbols is 7-bit ASCII, but 8-bit
character sequences are passed-through unchanged. Unicode/UCS data in UTF-8
@@ -1251,11 +1248,11 @@
to the standard collection of Isabelle regular symbols.
\<^medskip>
- Output of Isabelle symbols depends on the print mode. For example,
- the standard {\LaTeX} setup of the Isabelle document preparation system
- would present ``\<^verbatim>\<open>\<alpha>\<close>'' as \<open>\<alpha>\<close>, and ``\<^verbatim>\<open>\<^bold>\<alpha>\<close>'' as \<open>\<^bold>\<alpha>\<close>. On-screen rendering
- usually works by mapping a finite subset of Isabelle symbols to suitable
- Unicode characters.
+ Output of Isabelle symbols depends on the print mode. For example, the
+ standard {\LaTeX} setup of the Isabelle document preparation system would
+ present ``\<^verbatim>\<open>\<alpha>\<close>'' as \<open>\<alpha>\<close>, and ``\<^verbatim>\<open>\<^bold>\<alpha>\<close>'' as \<open>\<^bold>\<alpha>\<close>. On-screen rendering usually
+ works by mapping a finite subset of Isabelle symbols to suitable Unicode
+ characters.
\<close>
text %mlref \<open>
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Thu Oct 22 21:16:49 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Thu Oct 22 21:34:28 2015 +0200
@@ -135,7 +135,7 @@
argument that is a cartouche.
Omitting the control symbol is also possible: a cartouche without special
- decoration is equivalent to \<^verbatim>\<open>\\<close>\<^verbatim>\<open><^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which
+ decoration is equivalent to \<^verbatim>\<open>\<^cartouche>\<close>\<open>\<open>argument_content\<close>\<close>, which
is equivalent to \<^verbatim>\<open>@{cartouche\<close>~\<open>\<open>argument_content\<close>\<close>\<^verbatim>\<open>}\<close>. The
special name @{antiquotation_def cartouche} is defined in the context:
Isabelle/Pure introduces that as an alias to @{antiquotation_ref text}
--- a/src/Doc/JEdit/JEdit.thy Thu Oct 22 21:16:49 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy Thu Oct 22 21:34:28 2015 +0200
@@ -505,30 +505,26 @@
This is a summary for practically relevant input methods for Isabelle
symbols.
- \<^enum> The \<^emph>\<open>Symbols\<close> 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>\<open>symbol abbreviations\<close> (see below).
+ \<^enum> The \<^emph>\<open>Symbols\<close> 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>\<open>symbol
+ abbreviations\<close> (see below).
- \<^enum> 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.
+ \<^enum> 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.
- \<^enum> Copy/paste from prover output within Isabelle/jEdit. The same
- principles as for text buffers apply, but note that \<^emph>\<open>copy\<close> in secondary
- Isabelle/jEdit windows works via the keyboard shortcuts \<^verbatim>\<open>C+c\<close> or
- \<^verbatim>\<open>C+INSERT\<close>, while jEdit menu actions always refer to the primary
- text area!
+ \<^enum> Copy/paste from prover output within Isabelle/jEdit. The same principles
+ as for text buffers apply, but note that \<^emph>\<open>copy\<close> in secondary Isabelle/jEdit
+ windows works via the keyboard shortcuts \<^verbatim>\<open>C+c\<close> or \<^verbatim>\<open>C+INSERT\<close>, while jEdit
+ menu actions always refer to the primary text area!
- \<^enum> 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>\<open>\<lambda>\<close>, or its name preceded by backslash
- \<^verbatim>\<open>\\<close>\<^verbatim>\<open>lambda\<close>, or its ASCII abbreviation
- \<^verbatim>\<open>%\<close> by the Unicode rendering.
+ \<^enum> 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>\<open>\<lambda>\<close>, or its name preceded by backslash
+ \<^verbatim>\<open>\lambda\<close>, or its ASCII abbreviation \<^verbatim>\<open>%\<close> by the Unicode rendering.
The following table is an extract of the information provided by the
standard @{file "$ISABELLE_HOME/etc/symbols"} file:
@@ -565,13 +561,12 @@
\secref{sec:completion}).
- \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>\<open>Symbols\<close> 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.
+ \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>\<open>Symbols\<close> 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}
@@ -585,8 +580,7 @@
\<^medskip>
To produce a single control symbol, it is also possible to complete on
- \<^verbatim>\<open>\\<close>\<^verbatim>\<open>sup\<close>, \<^verbatim>\<open>\\<close>\<^verbatim>\<open>sub\<close>, \<^verbatim>\<open>\\<close>\<^verbatim>\<open>bold\<close>, \<^verbatim>\<open>\\<close>\<^verbatim>\<open>emph\<close> as for regular
- symbols.
+ \<^verbatim>\<open>\sup\<close>, \<^verbatim>\<open>\sub\<close>, \<^verbatim>\<open>\bold\<close>, \<^verbatim>\<open>\emph\<close> as for regular symbols.
The emphasized style only takes effect in document output, not in the
editor.
--- a/src/Doc/System/Presentation.thy Thu Oct 22 21:16:49 2015 +0200
+++ b/src/Doc/System/Presentation.thy Thu Oct 22 21:34:28 2015 +0200
@@ -233,7 +233,7 @@
includes an appropriate path specification for {\TeX} inputs.
If the text contains any references to Isabelle symbols (such as
- \<^verbatim>\<open>\\<close>\<^verbatim>\<open><forall>\<close>) then \<^verbatim>\<open>isabellesym.sty\<close> should be included as well.
+ \<^verbatim>\<open>\<forall>\<close>) then \<^verbatim>\<open>isabellesym.sty\<close> should be included as well.
This package contains a standard set of {\LaTeX} macro definitions
\<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>,
see @{cite "isabelle-implementation"} for a