src/Doc/Implementation/ML.thy

 
 
 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}
   variant & example & ML categories \\\hline
   lower-case & @{ML_text foo_bar} & values, types, record fields \\

 
   Name variants are produced by adding 1--3 primes, e.g.\ @{ML_text
   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
   typically shorter, sometimes using only rudiments of ``words'',
   while still avoiding cryptic shorthands.  An auxiliary function

 
   fun print_foo ctxt foo =
     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
   @{ML_text foo2bar}, nor @{ML_text bar_from_foo}, nor @{ML_text
   bar_for_foo}, nor @{ML_text bar4foo}).

 subsection \<open>General source layout\<close>
 
 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);
   val pair = (a, b);
   val record = {foo = 1, bar = 2};\<close>}

   Note that the space between @{ML_text g} and the pair @{ML_text
   "(a, b)"} follows the important principle of
   \<^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.
 
   Indentation follows a simple logical format that only depends on the

 
   \<^medskip>
   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},
   @{ML_text case} get extra indentation to indicate the nesting
   clearly.  Example:

 
 text \<open>The Standard ML semantics of strict functional evaluation
   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}
   exceptions can be handled internally, in order to be ignored, turned
   into other exceptions, or cascaded by appending messages.  If the

   Grammatical correctness of error messages can be improved by
   \<^emph>\<open>omitting\<close> final punctuation: messages are often concatenated
   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.
   Traditionally, the (short) exception message would include the name
   of an ML function, although this is no longer necessary, because the

   exceptions locally, e.g.\ to organize internal failures robustly
   without overlapping with existing exceptions.  Exceptions that are
   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,
   internal signaling of threads, or a POSIX process signal. An Isabelle/ML
   program that intercepts interrupts becomes dependent on physical effects of

   @{ML "Symbol.Sym"}, @{ML "Symbol.Control"}, @{ML "Symbol.Raw"},
   @{ML "Symbol.Malformed"}.
 
   \<^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>
 
 text \<open>The basis library proposal of SML97 needs to be treated with