--- a/src/Doc/Implementation/ML.thy Thu Oct 22 22:38:08 2015 +0200
+++ b/src/Doc/Implementation/ML.thy Thu Oct 22 23:01:49 2015 +0200
@@ -104,12 +104,12 @@
subsection \<open>Naming conventions\<close>
text \<open>Since ML is the primary medium to express the meaning of the
- source text, naming of ML entities requires special care.
-
- \paragraph{Notation.} A name consists of 1--3 \<^emph>\<open>words\<close> (rarely
- 4, but not more) that are separated by underscore. There are three
- variants concerning upper or lower case letters, which are used for
- certain ML categories as follows:
+ source text, naming of ML entities requires special care.\<close>
+
+paragraph \<open>Notation.\<close>
+text \<open>A name consists of 1--3 \<^emph>\<open>words\<close> (rarely 4, but not more) that are
+ separated by underscore. There are three variants concerning upper or lower
+ case letters, which are used for certain ML categories as follows:
\<^medskip>
\begin{tabular}{lll}
@@ -136,14 +136,15 @@
foo'}, @{ML_text foo''}, or @{ML_text foo'''}, but not @{ML_text
foo''''} or more. Decimal digits scale better to larger numbers,
e.g.\ @{ML_text foo0}, @{ML_text foo1}, @{ML_text foo42}.
-
- \paragraph{Scopes.} Apart from very basic library modules, ML
- structures are not ``opened'', but names are referenced with
- explicit qualification, as in @{ML Syntax.string_of_term} for
- example. When devising names for structures and their components it
- is important to aim at eye-catching compositions of both parts, because
- this is how they are seen in the sources and documentation. For the
- same reasons, aliases of well-known library functions should be
+\<close>
+
+paragraph\<open>Scopes.\<close>
+text \<open>Apart from very basic library modules, ML structures are not ``opened'',
+ but names are referenced with explicit qualification, as in @{ML
+ Syntax.string_of_term} for example. When devising names for structures and
+ their components it is important to aim at eye-catching compositions of both
+ parts, because this is how they are seen in the sources and documentation.
+ For the same reasons, aliases of well-known library functions should be
avoided.
Local names of function abstraction or case/let bindings are
@@ -180,10 +181,10 @@
let
fun aux t = ... string_of_term ctxt t ...
in ... end;\<close>}
-
-
- \paragraph{Specific conventions.} Here are some specific name forms
- that occur frequently in the sources.
+\<close>
+
+paragraph \<open>Specific conventions.\<close>
+text \<open>Here are some specific name forms that occur frequently in the sources.
\<^item> A function that maps @{ML_text foo} to @{ML_text bar} is
called @{ML_text foo_to_bar} or @{ML_text bar_of_foo} (never
@@ -274,22 +275,22 @@
text \<open>
The general Isabelle/ML source layout imitates regular type-setting
conventions, augmented by the requirements for deeply nested expressions
- that are commonplace in functional programming.
-
- \paragraph{Line length} is limited to 80 characters according to ancient
- standards, but we allow as much as 100 characters (not
- more).\footnote{Readability requires to keep the beginning of a line
- in view while watching its end. Modern wide-screen displays do not
- change the way how the human brain works. Sources also need to be
- printable on plain paper with reasonable font-size.} The extra 20
- characters acknowledge the space requirements due to qualified
- library references in Isabelle/ML.
-
- \paragraph{White-space} is used to emphasize the structure of
- expressions, following mostly standard conventions for mathematical
- typesetting, as can be seen in plain {\TeX} or {\LaTeX}. This
- defines positioning of spaces for parentheses, punctuation, and
- infixes as illustrated here:
+ that are commonplace in functional programming.\<close>
+
+paragraph \<open>Line length\<close>
+text \<open>is limited to 80 characters according to ancient standards, but we allow
+ as much as 100 characters (not more).\footnote{Readability requires to keep
+ the beginning of a line in view while watching its end. Modern wide-screen
+ displays do not change the way how the human brain works. Sources also need
+ to be printable on plain paper with reasonable font-size.} The extra 20
+ characters acknowledge the space requirements due to qualified library
+ references in Isabelle/ML.\<close>
+
+paragraph \<open>White-space\<close>
+text \<open>is used to emphasize the structure of expressions, following mostly
+ standard conventions for mathematical typesetting, as can be seen in plain
+ {\TeX} or {\LaTeX}. This defines positioning of spaces for parentheses,
+ punctuation, and infixes as illustrated here:
@{verbatim [display]
\<open> val x = y + z * (a + b);
@@ -323,13 +324,14 @@
\<^emph>\<open>compositionality\<close>: the layout of @{ML_text "g p"} does not
change when @{ML_text "p"} is refined to the concrete pair
@{ML_text "(a, b)"}.
-
- \paragraph{Indentation} uses plain spaces, never hard
- tabulators.\footnote{Tabulators were invented to move the carriage
- of a type-writer to certain predefined positions. In software they
- could be used as a primitive run-length compression of consecutive
- spaces, but the precise result would depend on non-standardized
- text editor configuration.}
+\<close>
+
+paragraph \<open>Indentation\<close>
+text \<open>uses plain spaces, never hard tabulators.\footnote{Tabulators were
+ invented to move the carriage of a type-writer to certain predefined
+ positions. In software they could be used as a primitive run-length
+ compression of consecutive spaces, but the precise result would depend on
+ non-standardized text editor configuration.}
Each level of nesting is indented by 2 spaces, sometimes 1, very
rarely 4, never 8 or any other odd number.
@@ -367,11 +369,13 @@
For similar reasons, any kind of two-dimensional or tabular
layouts, ASCII-art with lines or boxes of asterisks etc.\ should be
avoided.
-
- \paragraph{Complex expressions} that consist of multi-clausal
- function definitions, @{ML_text handle}, @{ML_text case},
- @{ML_text let} (and combinations) require special attention. The
- syntax of Standard ML is quite ambitious and admits a lot of
+\<close>
+
+paragraph \<open>Complex expressions\<close>
+
+text \<open>that consist of multi-clausal function definitions, @{ML_text handle},
+ @{ML_text case}, @{ML_text let} (and combinations) require special
+ attention. The syntax of Standard ML is quite ambitious and admits a lot of
variance that can distort the meaning of the text.
Multiple clauses of @{ML_text fun}, @{ML_text fn}, @{ML_text handle},
@@ -1083,10 +1087,11 @@
together with exceptions is rather well defined, but some delicate
points need to be observed to avoid that ML programs go wrong
despite static type-checking. Exceptions in Isabelle/ML are
- subsequently categorized as follows.
-
- \paragraph{Regular user errors.} These are meant to provide
- informative feedback about malformed input etc.
+ subsequently categorized as follows.\<close>
+
+paragraph \<open>Regular user errors.\<close>
+text \<open>These are meant to provide informative feedback about malformed input
+ etc.
The \<^emph>\<open>error\<close> function raises the corresponding @{ML ERROR}
exception, with a plain text message as argument. @{ML ERROR}
@@ -1105,11 +1110,12 @@
or put into a larger context (e.g.\ augmented with source position).
Note that punctuation after formal entities (types, terms, theorems) is
particularly prone to user confusion.
-
- \paragraph{Program failures.} There is a handful of standard
- exceptions that indicate general failure situations, or failures of
- core operations on logical entities (types, terms, theorems,
- theories, see \chref{ch:logic}).
+\<close>
+
+paragraph \<open>Program failures.\<close>
+text \<open>There is a handful of standard exceptions that indicate general failure
+ situations, or failures of core operations on logical entities (types,
+ terms, theorems, theories, see \chref{ch:logic}).
These exceptions indicate a genuine breakdown of the program, so the
main purpose is to determine quickly what has happened where.
@@ -1125,11 +1131,12 @@
exposed in module signatures require extra care, though, and should
\<^emph>\<open>not\<close> be introduced by default. Surprise by users of a module
can be often minimized by using plain user errors instead.
-
- \paragraph{Interrupts.} These indicate arbitrary system events:
- both the ML runtime system and the Isabelle/ML infrastructure signal
- various exceptional situations by raising the special
- @{ML Exn.Interrupt} exception in user code.
+\<close>
+
+paragraph \<open>Interrupts.\<close>
+text \<open>These indicate arbitrary system events: both the ML runtime system and
+ the Isabelle/ML infrastructure signal various exceptional situations by
+ raising the special @{ML Exn.Interrupt} exception in user code.
This is the one and only way that physical events can intrude an Isabelle/ML
program. Such an interrupt can mean out-of-memory, stack overflow, timeout,
@@ -1292,19 +1299,18 @@
\<^descr> @{ML "Symbol.decode"} converts the string representation of a
symbol into the datatype version.
-
-
- \paragraph{Historical note.} In the original SML90 standard the
- primitive ML type @{ML_type char} did not exists, and @{ML_text
- "explode: string -> string list"} produced a list of singleton
- strings like @{ML "raw_explode: string -> string list"} in
- Isabelle/ML today. When SML97 came out, Isabelle did not adopt its
- somewhat anachronistic 8-bit or 16-bit characters, but the idea of
- exploding a string into a list of small strings was extended to
- ``symbols'' as explained above. Thus Isabelle sources can refer to
- an infinite store of user-defined symbols, without having to worry
- about the multitude of Unicode encodings that have emerged over the
- years.\<close>
+\<close>
+
+paragraph \<open>Historical note.\<close>
+text \<open>In the original SML90 standard the primitive ML type @{ML_type char} did
+ not exists, and @{ML_text "explode: string -> string list"} produced a list
+ of singleton strings like @{ML "raw_explode: string -> string list"} in
+ Isabelle/ML today. When SML97 came out, Isabelle did not adopt its somewhat
+ anachronistic 8-bit or 16-bit characters, but the idea of exploding a string
+ into a list of small strings was extended to ``symbols'' as explained above.
+ Thus Isabelle sources can refer to an infinite store of user-defined
+ symbols, without having to worry about the multitude of Unicode encodings
+ that have emerged over the years.\<close>
section \<open>Basic data types\<close>
--- a/src/Doc/Implementation/Prelim.thy Thu Oct 22 22:38:08 2015 +0200
+++ b/src/Doc/Implementation/Prelim.thy Thu Oct 22 23:01:49 2015 +0200
@@ -276,10 +276,10 @@
text \<open>The main purpose of theory and proof contexts is to manage
arbitrary (pure) data. New data types can be declared incrementally
at compile time. There are separate declaration mechanisms for any
- of the three kinds of contexts: theory, proof, generic.
+ of the three kinds of contexts: theory, proof, generic.\<close>
- \paragraph{Theory data} declarations need to implement the following
- ML signature:
+paragraph \<open>Theory data\<close>
+text \<open>declarations need to implement the following ML signature:
\<^medskip>
\begin{tabular}{ll}
@@ -302,9 +302,10 @@
Particularly note that shared parts of the data must not be
duplicated by naive concatenation, or a theory graph that is like a
chain of diamonds would cause an exponential blowup!
+\<close>
- \paragraph{Proof context data} declarations need to implement the
- following ML signature:
+paragraph \<open>Proof context data\<close>
+text \<open>declarations need to implement the following ML signature:
\<^medskip>
\begin{tabular}{ll}
@@ -323,11 +324,12 @@
at most one, sometimes two data slots for its internal use.
Repeated data declarations to simulate a record type should be
avoided!
+\<close>
- \paragraph{Generic data} provides a hybrid interface for both theory
- and proof data. The \<open>init\<close> operation for proof contexts is
- predefined to select the current data value from the background
- theory.
+paragraph \<open>Generic data\<close>
+text \<open>provides a hybrid interface for both theory and proof data. The \<open>init\<close>
+ operation for proof contexts is predefined to select the current data
+ value from the background theory.
\<^bigskip>
Any of the above data declarations over type \<open>T\<close>
--- a/src/Doc/JEdit/JEdit.thy Thu Oct 22 22:38:08 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy Thu Oct 22 23:01:49 2015 +0200
@@ -461,26 +461,26 @@
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.
+\<close>
- \<^medskip>
- \paragraph{Encoding.} Technically, the Unicode view on Isabelle
- symbols is an \<^emph>\<open>encoding\<close> called \<^verbatim>\<open>UTF-8-Isabelle\<close> in jEdit
- (not in the underlying JVM). 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>\<open>ISO-8859-15\<close>. In that case,
- verbatim ``\<^verbatim>\<open>\<alpha>\<close>'' will be shown in the text buffer instead of its
- Unicode rendering ``\<open>\<alpha>\<close>''. The jEdit menu operation \<^emph>\<open>File~/
- Reload with Encoding~/ UTF-8-Isabelle\<close> helps to resolve such problems (after
- repairing malformed parts of the text).
+paragraph \<open>Encoding.\<close>
+text \<open>Technically, the Unicode view on Isabelle symbols is an \<^emph>\<open>encoding\<close>
+ called \<^verbatim>\<open>UTF-8-Isabelle\<close> in jEdit (not in the underlying JVM). 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>\<open>ISO-8859-15\<close>. In that case, verbatim ``\<^verbatim>\<open>\<alpha>\<close>'' will be shown in the text
+ buffer instead of its Unicode rendering ``\<open>\<alpha>\<close>''. The jEdit menu operation
+ \<^emph>\<open>File~/ Reload with Encoding~/ UTF-8-Isabelle\<close> helps to resolve such
+ problems (after repairing malformed parts of the text).
+\<close>
- \<^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>\<open>IsabelleText\<close>, which ensures that
- standard collection of Isabelle symbols are actually seen on the
- screen (or printer).
+paragraph \<open>Font.\<close>
+text \<open>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>\<open>IsabelleText\<close>, 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 outdated
@@ -491,16 +491,16 @@
This problem can be avoided by refraining to ``install'' any version of
\<^verbatim>\<open>IsabelleText\<close> in the first place, although it is occasionally
tempting to use the same font in other applications.
+\<close>
- \<^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>\<open>input methods\<close>. Regular jEdit also provides various ways to
- work with \<^emph>\<open>abbreviations\<close> 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.
+paragraph \<open>Input methods.\<close>
+text \<open>In principle, Isabelle/jEdit could delegate the problem to produce
+ Isabelle symbols in their Unicode rendering to the underlying operating
+ system and its \<^emph>\<open>input methods\<close>. Regular jEdit also provides various ways to
+ work with \<^emph>\<open>abbreviations\<close> 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.
This is a summary for practically relevant input methods for Isabelle
symbols.
@@ -559,14 +559,15 @@
replacement syntax syntax helps to update old theory sources via
explicit completion (see also \<^verbatim>\<open>C+b\<close> explained in
\secref{sec:completion}).
-
+\<close>
- \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 \<open>Control symbols.\<close>
+text \<open>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}