author wenzelm Fri, 22 Oct 2010 11:27:05 +0100 changeset 39879 be8a7334e4ec parent 39878 31dd361a3060 child 39880 7deb6a741626
tuned;
--- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Oct 21 21:53:34 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Fri Oct 22 11:27:05 2010 +0100
@@ -30,49 +30,40 @@

section {* Style and orthography *}

-text {* The sources Isabelle/Isar implementation are optimized for
-  \emph{readability} and \emph{maintainability}.  The main purpose of
-  the sources is to tell an informed reader what is really going on
-  and how things really work.  This is a non-trivial aim, but it
-  greatly helps to follow a certain style for Isabelle/ML that has
-  emerged from long years of Isabelle system development.\footnote{See
-  also the very interesting style guide for OCaml
+text {* The sources of Isabelle/Isar are optimized for
+  \emph{readability} and \emph{maintainability}.  The main purpose is
+  to tell an informed reader what is really going on and how things
+  really work.  This is a non-trivial aim, but it is supported by a
+  certain style of writing Isabelle/ML that has emerged from long
+  guide for OCaml
\url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}
which shares many of our means and ends.}

The main principle behind any coding style is \emph{consistency}.
-  For a single author and a small project this merely means choose
+  For a single author of a small program this merely means choose
your style and stick to it''.  A complex project like Isabelle, with
-  long years of development and different contributors this requires
-  more and more standardization.  A coding style that is changed every
-  few years or with every new contributor is no style at all, because
-  consistency is quickly lost.  Global consistency is hard to achieve,
-  but one should always strife at least for local consistency of
-  modules and sub-systems, without deviating from some general
-  principles how to write Isabelle/ML.
+  long years of development and different contributors, requires more
+  standardization.  A coding style that is changed every few years or
+  with every new contributor is no style at all, because consistency
+  is quickly lost.  Global consistency is hard to achieve, though.
+  One should always strife at least for local consistency of modules
+  and sub-systems, without deviating from some general principles how
+  to write Isabelle/ML.

In a sense, a common coding style is like an \emph{orthography} for
-  the sources: it helps to read quickly over it and see through the
-  main points, without getting distracted by accidental presentation
-  of free-style text.
-*}
-
-
-subsection {* Basic naming conventions *}
-
-text {* Since ML is the primary medium to express the meaning of the
-  source text, naming of ML entities requires special care.
-
-  FIXME
+  the sources: it helps to read quickly over the text and see through
+  the main points, without getting distracted by accidental
+  presentation of free-style source.
*}

subsection {* Header and sectioning *}

-text {* Isabelle source files have a certain standardized header that
-  follows ancient traditions back to the earliest versions of the
-  system by Larry Paulson (including precise spacing).  E.g.\ see
-  @{"file" "~~/src/Pure/thm.ML"}.
+text {* Isabelle source files have a certain standardized header
+  format (with precise spacing) that follows ancient traditions
+  reaching back to the earliest versions of the system by Larry
+  Paulson.  E.g.\ see @{"file" "~~/src/Pure/thm.ML"}.

The header includes at least @{verbatim Title} and @{verbatim
Author} entries, followed by a prose description of the purpose of
@@ -80,8 +71,8 @@
paragraphs of explanations.

The rest of the file is divided into sections, subsections,
-  subsubsections, paragraphs etc.\ using some simple layout via ML
+  subsubsections, paragraphs etc.\ using some a layout via ML comments
+  as follows.

\begin{verbatim}
(*** section ***)
@@ -103,8 +94,17 @@
as in the example above).

\medskip The precise wording of the prose text given in these
-  headings is chosen carefully to indicate the main theme of what is
-  coming next in the formal ML text.
+  headings is chosen carefully to indicate the main theme of the
+  subsequent formal ML text.
+*}
+
+
+subsection {* Basic naming conventions *}
+
+text {* Since ML is the primary medium to express the meaning of the
+  source text, naming of ML entities requires special care.
+
+  FIXME
*}

@@ -116,15 +116,15 @@
programming.

\paragraph{Line length} is 80 characters according to ancient
-  standards, but we allow as much as 100 characters to acknowledge the
-  extra space requirements due to the relatively long fully-qualified
-  library references in Isabelle/ML.
+  standards, but we allow as much as 100 characters, not more.  This
+  acknowledges extra 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, infixes
-  as illustrated here:
+  defines positioning of spaces for parentheses, punctuation, and
+  infixes as illustrated here:

\begin{verbatim}
val x = y + z * (a + b);
@@ -132,8 +132,8 @@
val record = {foo = 1, bar = 2};
\end{verbatim}

-  Lines are normally broken after an infix operator or punctuation
-  character.  E.g.\
+  Lines are normally broken \emph{after} an infix operator or
+  punctuation character.  For example:

\begin{verbatim}
val x =
@@ -148,15 +148,15 @@
\end{verbatim}

Some special infixes (e.g.\ @{verbatim "|>"}) work better at the
-  start of the line.  For punctuation there are no such exceptions.
+  start of the line, but punctuation is always at the end.

Function application follows the tradition of @{text "\<lambda>"}-calculus,
not informal mathematics.  For example: @{verbatim "f a b"} for a
curried function, or @{verbatim "g (a, b)"} for a tupled function.
Note that the space between @{verbatim g} and the pair @{verbatim
-  "(a, b)"} follows the important principle of compositionality: the
-  layout of @{verbatim "g p"} does not change when @{verbatim "p"} is
-  refined to a concrete pair.
+  "(a, b)"} follows the important principle of
+  \emph{compositionality}: the layout of @{verbatim "g p"} does not
+  change when @{verbatim "p"} is refined to a concrete pair.

\paragraph{Indentation} uses plain spaces, never hard
tabulators.\footnote{Tabulators were invented to move the carriage
@@ -165,37 +165,39 @@
spaces, but the precise result would depend on non-standardized
editor configuration.}

-  Each level of logical nesting is indented by 2 spaces, sometimes 1;
-  very rarely 4, never 8.
+  Each level of nesting is indented by 2 spaces, sometimes 1, very
+  rarely 4, never 8.

-  Indentation follows the simple logical form'' that only depends on
-  the nesting depth, not the accidental length of the text that
-  initiates a level of nesting.  Example:
+  Indentation follows a simple logical format that only depends on the
+  nesting depth, not the accidental length of the text that initiates
+  a level of nesting.  Example:

\begin{verbatim}
-  (*right*)
+  (*RIGHT*)
if b then
-    expr1
+    expr1_part1
+    expr1_part2
else
-    expr2
+    expr2_part1
+    expr2_part2

-  (*wrong*)
-  if b then
-            expr1
-  else
-            expr2
+  (*WRONG*)
+  if b then expr1_part1
+            expr1_part2
+  else expr2_part1
+       expr2_part2
\end{verbatim}

The second form has many problems: it assumes a fixed-width font
-  when viewing the sources, it uses more space on the line and makes
-  it hard to observe its strict length limit (working against
+  when viewing the sources, it uses more space on the line and thus
+  makes it hard to observe its strict length limit (working against