diff -r a4478ca660a5 -r 436b7fe89cdc src/Doc/Implementation/ML.thy --- 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 \Naming conventions\ text \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>\words\ (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.\ + +paragraph \Notation.\ +text \A name consists of 1--3 \<^emph>\words\ (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 +\ + +paragraph\Scopes.\ +text \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;\} - - - \paragraph{Specific conventions.} Here are some specific name forms - that occur frequently in the sources. +\ + +paragraph \Specific conventions.\ +text \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 \ 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.\ + +paragraph \Line length\ +text \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\ +text \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] \ val x = y + z * (a + b); @@ -323,13 +324,14 @@ \<^emph>\compositionality\: 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.} +\ + +paragraph \Indentation\ +text \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 +\ + +paragraph \Complex expressions\ + +text \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.\ + +paragraph \Regular user errors.\ +text \These are meant to provide informative feedback about malformed input + etc. The \<^emph>\error\ 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}). +\ + +paragraph \Program failures.\ +text \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>\not\ 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. +\ + +paragraph \Interrupts.\ +text \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.\ +\ + +paragraph \Historical note.\ +text \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.\ section \Basic data types\