--- 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
+ years of system development.\footnote{See also the interesting style
+ 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
- comments as follows.
+ 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
\emph{readability}), it requires extra editing to adapt the layout
- to changes of the initial expression @{verbatim b} (working against
+ to changes of the initial text (working against
\emph{maintainability}) etc.
- \medskip Any kind of two-dimensional or tabular layouts, ASCII-art
- with lines or boxes of stars etc. should be avoided for the same
- reasons.
+ \medskip For similar reasons, any kind of two-dimensional or tabular
+ layouts, ASCII-art with lines or boxes of stars etc. should be
+ avoided.
*}