28 merely reflect snapshots that are never really up-to-date.} *} |
28 merely reflect snapshots that are never really up-to-date.} *} |
29 |
29 |
30 |
30 |
31 section {* Style and orthography *} |
31 section {* Style and orthography *} |
32 |
32 |
33 text {* The sources Isabelle/Isar implementation are optimized for |
33 text {* The sources of Isabelle/Isar are optimized for |
34 \emph{readability} and \emph{maintainability}. The main purpose of |
34 \emph{readability} and \emph{maintainability}. The main purpose is |
35 the sources is to tell an informed reader what is really going on |
35 to tell an informed reader what is really going on and how things |
36 and how things really work. This is a non-trivial aim, but it |
36 really work. This is a non-trivial aim, but it is supported by a |
37 greatly helps to follow a certain style for Isabelle/ML that has |
37 certain style of writing Isabelle/ML that has emerged from long |
38 emerged from long years of Isabelle system development.\footnote{See |
38 years of system development.\footnote{See also the interesting style |
39 also the very interesting style guide for OCaml |
39 guide for OCaml |
40 \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html} |
40 \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html} |
41 which shares many of our means and ends.} |
41 which shares many of our means and ends.} |
42 |
42 |
43 The main principle behind any coding style is \emph{consistency}. |
43 The main principle behind any coding style is \emph{consistency}. |
44 For a single author and a small project this merely means ``choose |
44 For a single author of a small program this merely means ``choose |
45 your style and stick to it''. A complex project like Isabelle, with |
45 your style and stick to it''. A complex project like Isabelle, with |
46 long years of development and different contributors this requires |
46 long years of development and different contributors, requires more |
47 more and more standardization. A coding style that is changed every |
47 standardization. A coding style that is changed every few years or |
48 few years or with every new contributor is no style at all, because |
48 with every new contributor is no style at all, because consistency |
49 consistency is quickly lost. Global consistency is hard to achieve, |
49 is quickly lost. Global consistency is hard to achieve, though. |
50 but one should always strife at least for local consistency of |
50 One should always strife at least for local consistency of modules |
51 modules and sub-systems, without deviating from some general |
51 and sub-systems, without deviating from some general principles how |
52 principles how to write Isabelle/ML. |
52 to write Isabelle/ML. |
53 |
53 |
54 In a sense, a common coding style is like an \emph{orthography} for |
54 In a sense, a common coding style is like an \emph{orthography} for |
55 the sources: it helps to read quickly over it and see through the |
55 the sources: it helps to read quickly over the text and see through |
56 main points, without getting distracted by accidental presentation |
56 the main points, without getting distracted by accidental |
57 of free-style text. |
57 presentation of free-style source. |
58 *} |
|
59 |
|
60 |
|
61 subsection {* Basic naming conventions *} |
|
62 |
|
63 text {* Since ML is the primary medium to express the meaning of the |
|
64 source text, naming of ML entities requires special care. |
|
65 |
|
66 FIXME |
|
67 *} |
58 *} |
68 |
59 |
69 |
60 |
70 subsection {* Header and sectioning *} |
61 subsection {* Header and sectioning *} |
71 |
62 |
72 text {* Isabelle source files have a certain standardized header that |
63 text {* Isabelle source files have a certain standardized header |
73 follows ancient traditions back to the earliest versions of the |
64 format (with precise spacing) that follows ancient traditions |
74 system by Larry Paulson (including precise spacing). E.g.\ see |
65 reaching back to the earliest versions of the system by Larry |
75 @{"file" "~~/src/Pure/thm.ML"}. |
66 Paulson. E.g.\ see @{"file" "~~/src/Pure/thm.ML"}. |
76 |
67 |
77 The header includes at least @{verbatim Title} and @{verbatim |
68 The header includes at least @{verbatim Title} and @{verbatim |
78 Author} entries, followed by a prose description of the purpose of |
69 Author} entries, followed by a prose description of the purpose of |
79 the module. The latter can range from a single line to several |
70 the module. The latter can range from a single line to several |
80 paragraphs of explanations. |
71 paragraphs of explanations. |
81 |
72 |
82 The rest of the file is divided into sections, subsections, |
73 The rest of the file is divided into sections, subsections, |
83 subsubsections, paragraphs etc.\ using some simple layout via ML |
74 subsubsections, paragraphs etc.\ using some a layout via ML comments |
84 comments as follows. |
75 as follows. |
85 |
76 |
86 \begin{verbatim} |
77 \begin{verbatim} |
87 (*** section ***) |
78 (*** section ***) |
88 |
79 |
89 (** subsection **) |
80 (** subsection **) |
101 As in regular typography, there is some extra space \emph{before} |
92 As in regular typography, there is some extra space \emph{before} |
102 section headings that are adjacent to plain text (not other headings |
93 section headings that are adjacent to plain text (not other headings |
103 as in the example above). |
94 as in the example above). |
104 |
95 |
105 \medskip The precise wording of the prose text given in these |
96 \medskip The precise wording of the prose text given in these |
106 headings is chosen carefully to indicate the main theme of what is |
97 headings is chosen carefully to indicate the main theme of the |
107 coming next in the formal ML text. |
98 subsequent formal ML text. |
|
99 *} |
|
100 |
|
101 |
|
102 subsection {* Basic naming conventions *} |
|
103 |
|
104 text {* Since ML is the primary medium to express the meaning of the |
|
105 source text, naming of ML entities requires special care. |
|
106 |
|
107 FIXME |
108 *} |
108 *} |
109 |
109 |
110 |
110 |
111 subsection {* General source layout *} |
111 subsection {* General source layout *} |
112 |
112 |
114 type-setting to some extent, augmented by the requirements for |
114 type-setting to some extent, augmented by the requirements for |
115 deeply nested expressions that are commonplace in functional |
115 deeply nested expressions that are commonplace in functional |
116 programming. |
116 programming. |
117 |
117 |
118 \paragraph{Line length} is 80 characters according to ancient |
118 \paragraph{Line length} is 80 characters according to ancient |
119 standards, but we allow as much as 100 characters to acknowledge the |
119 standards, but we allow as much as 100 characters, not more. This |
120 extra space requirements due to the relatively long fully-qualified |
120 acknowledges extra the space requirements due to qualified library |
121 library references in Isabelle/ML. |
121 references in Isabelle/ML. |
122 |
122 |
123 \paragraph{White-space} is used to emphasize the structure of |
123 \paragraph{White-space} is used to emphasize the structure of |
124 expressions, following mostly standard conventions for mathematical |
124 expressions, following mostly standard conventions for mathematical |
125 typesetting, as can be seen in plain {\TeX} or {\LaTeX}. This |
125 typesetting, as can be seen in plain {\TeX} or {\LaTeX}. This |
126 defines positioning of spaces for parentheses, punctuation, infixes |
126 defines positioning of spaces for parentheses, punctuation, and |
127 as illustrated here: |
127 infixes as illustrated here: |
128 |
128 |
129 \begin{verbatim} |
129 \begin{verbatim} |
130 val x = y + z * (a + b); |
130 val x = y + z * (a + b); |
131 val pair = (a, b); |
131 val pair = (a, b); |
132 val record = {foo = 1, bar = 2}; |
132 val record = {foo = 1, bar = 2}; |
133 \end{verbatim} |
133 \end{verbatim} |
134 |
134 |
135 Lines are normally broken after an infix operator or punctuation |
135 Lines are normally broken \emph{after} an infix operator or |
136 character. E.g.\ |
136 punctuation character. For example: |
137 |
137 |
138 \begin{verbatim} |
138 \begin{verbatim} |
139 val x = |
139 val x = |
140 a + |
140 a + |
141 b + |
141 b + |
146 b, |
146 b, |
147 c); |
147 c); |
148 \end{verbatim} |
148 \end{verbatim} |
149 |
149 |
150 Some special infixes (e.g.\ @{verbatim "|>"}) work better at the |
150 Some special infixes (e.g.\ @{verbatim "|>"}) work better at the |
151 start of the line. For punctuation there are no such exceptions. |
151 start of the line, but punctuation is always at the end. |
152 |
152 |
153 Function application follows the tradition of @{text "\<lambda>"}-calculus, |
153 Function application follows the tradition of @{text "\<lambda>"}-calculus, |
154 not informal mathematics. For example: @{verbatim "f a b"} for a |
154 not informal mathematics. For example: @{verbatim "f a b"} for a |
155 curried function, or @{verbatim "g (a, b)"} for a tupled function. |
155 curried function, or @{verbatim "g (a, b)"} for a tupled function. |
156 Note that the space between @{verbatim g} and the pair @{verbatim |
156 Note that the space between @{verbatim g} and the pair @{verbatim |
157 "(a, b)"} follows the important principle of compositionality: the |
157 "(a, b)"} follows the important principle of |
158 layout of @{verbatim "g p"} does not change when @{verbatim "p"} is |
158 \emph{compositionality}: the layout of @{verbatim "g p"} does not |
159 refined to a concrete pair. |
159 change when @{verbatim "p"} is refined to a concrete pair. |
160 |
160 |
161 \paragraph{Indentation} uses plain spaces, never hard |
161 \paragraph{Indentation} uses plain spaces, never hard |
162 tabulators.\footnote{Tabulators were invented to move the carriage |
162 tabulators.\footnote{Tabulators were invented to move the carriage |
163 of a type-writer to certain predefined positions. In software they |
163 of a type-writer to certain predefined positions. In software they |
164 could be used as a primitive run-length compression of consecutive |
164 could be used as a primitive run-length compression of consecutive |
165 spaces, but the precise result would depend on non-standardized |
165 spaces, but the precise result would depend on non-standardized |
166 editor configuration.} |
166 editor configuration.} |
167 |
167 |
168 Each level of logical nesting is indented by 2 spaces, sometimes 1; |
168 Each level of nesting is indented by 2 spaces, sometimes 1, very |
169 very rarely 4, never 8. |
169 rarely 4, never 8. |
170 |
170 |
171 Indentation follows the simple ``logical form'' that only depends on |
171 Indentation follows a simple logical format that only depends on the |
172 the nesting depth, not the accidental length of the text that |
172 nesting depth, not the accidental length of the text that initiates |
173 initiates a level of nesting. Example: |
173 a level of nesting. Example: |
174 |
174 |
175 \begin{verbatim} |
175 \begin{verbatim} |
176 (*right*) |
176 (*RIGHT*) |
177 if b then |
177 if b then |
178 expr1 |
178 expr1_part1 |
|
179 expr1_part2 |
179 else |
180 else |
180 expr2 |
181 expr2_part1 |
181 |
182 expr2_part2 |
182 (*wrong*) |
183 |
183 if b then |
184 (*WRONG*) |
184 expr1 |
185 if b then expr1_part1 |
185 else |
186 expr1_part2 |
186 expr2 |
187 else expr2_part1 |
|
188 expr2_part2 |
187 \end{verbatim} |
189 \end{verbatim} |
188 |
190 |
189 The second form has many problems: it assumes a fixed-width font |
191 The second form has many problems: it assumes a fixed-width font |
190 when viewing the sources, it uses more space on the line and makes |
192 when viewing the sources, it uses more space on the line and thus |
191 it hard to observe its strict length limit (working against |
193 makes it hard to observe its strict length limit (working against |
192 \emph{readability}), it requires extra editing to adapt the layout |
194 \emph{readability}), it requires extra editing to adapt the layout |
193 to changes of the initial expression @{verbatim b} (working against |
195 to changes of the initial text (working against |
194 \emph{maintainability}) etc. |
196 \emph{maintainability}) etc. |
195 |
197 |
196 \medskip Any kind of two-dimensional or tabular layouts, ASCII-art |
198 \medskip For similar reasons, any kind of two-dimensional or tabular |
197 with lines or boxes of stars etc. should be avoided for the same |
199 layouts, ASCII-art with lines or boxes of stars etc. should be |
198 reasons. |
200 avoided. |
199 *} |
201 *} |
200 |
202 |
201 |
203 |
202 section {* SML embedded into Isabelle/Isar *} |
204 section {* SML embedded into Isabelle/Isar *} |
203 |
205 |