--- 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>