# HG changeset patch # User wenzelm # Date 1287743225 -3600 # Node ID be8a7334e4ecfc807ded079730f4747feebf39cc # Parent 31dd361a30609a77c44e03e58d7214ef8491a689 tuned; diff -r 31dd361a3060 -r be8a7334e4ec doc-src/IsarImplementation/Thy/ML.thy --- 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 "\"}-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. *}