author | haftmann |
Wed, 12 Dec 2007 09:00:07 +0100 | |
changeset 25608 | 7793d6423d01 |
parent 25185 | 762ed22d15c7 |
child 26437 | 5906619c8c6b |
permissions | -rw-r--r-- |
18537 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{ML}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
\isanewline |
|
18543 | 7 |
\isanewline |
18537 | 8 |
% |
9 |
\endisadelimtheory |
|
10 |
% |
|
11 |
\isatagtheory |
|
12 |
\isacommand{theory}\isamarkupfalse% |
|
18543 | 13 |
\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}% |
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupchapter{Aesthetics of ML programming% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
24089 | 25 |
\isamarkupsection{Style% |
26 |
} |
|
27 |
\isamarkuptrue% |
|
28 |
% |
|
18543 | 29 |
\begin{isamarkuptext}% |
21501 | 30 |
FIXME% |
31 |
\end{isamarkuptext}% |
|
32 |
\isamarkuptrue% |
|
33 |
% |
|
34 |
\begin{isamarkuptext}% |
|
21148 | 35 |
This style guide is loosely based on |
36 |
\url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}. |
|
37 |
% FIMXE \url{http://www.cs.cornell.edu/Courses/cs312/2003sp/handouts/style.htm} |
|
38 |
||
24089 | 39 |
Like any style guide, it should not be interpreted dogmatically, but |
40 |
with care and discernment. Instead, it forms a collection of |
|
41 |
recommendations which, if obeyed, result in code that is not |
|
42 |
considered to be obfuscated. In certain cases, derivations are |
|
43 |
encouraged, as far as you know what you are doing. |
|
21148 | 44 |
|
45 |
\begin{description} |
|
46 |
||
47 |
\item[fundamental law of programming] |
|
48 |
Whenever writing code, keep in mind: A program is |
|
49 |
written once, modified ten times, and read |
|
50 |
100 times. So simplify its writing, |
|
51 |
always keep future modifications in mind, |
|
21172 | 52 |
and never jeopardize readability. Every second you hesitate |
21148 | 53 |
to spend on making your code more clear you will |
54 |
have to spend ten times understanding what you have |
|
55 |
written later on. |
|
56 |
||
57 |
\item[white space matters] |
|
58 |
Treat white space in your code as if it determines |
|
59 |
the meaning of code. |
|
60 |
||
61 |
\begin{itemize} |
|
62 |
||
63 |
\item The space bar is the easiest key to find on the keyboard, |
|
24089 | 64 |
press it as often as necessary. \verb|2 + 2| is better |
65 |
than \verb|2+2|, likewise \verb|f (x, y)| is |
|
66 |
better than \verb|f(x,y)|. |
|
21148 | 67 |
|
24089 | 68 |
\item Restrict your lines to 80 characters. This will allow |
69 |
you to keep the beginning of a line in view while watching |
|
70 |
its end.\footnote{To acknowledge the lax practice of |
|
71 |
text editing these days, we tolerate as much as 100 |
|
72 |
characters per line, but anything beyond 120 is not |
|
73 |
considered proper source text.} |
|
21148 | 74 |
|
24089 | 75 |
\item Ban tabulators; they are a context-sensitive formatting |
76 |
feature and likely to confuse anyone not using your favorite |
|
77 |
editor.\footnote{Some modern programming language even |
|
78 |
forbid tabulators altogether according to the formal syntax |
|
79 |
definition.} |
|
21148 | 80 |
|
81 |
\item Get rid of trailing whitespace. Instead, do not |
|
24089 | 82 |
suppress a trailing newline at the end of your files. |
21148 | 83 |
|
84 |
\item Choose a generally accepted style of indentation, |
|
85 |
then use it systematically throughout the whole |
|
86 |
application. An indentation of two spaces is appropriate. |
|
87 |
Avoid dangling indentation. |
|
88 |
||
89 |
\end{itemize} |
|
90 |
||
91 |
\item[cut-and-paste succeeds over copy-and-paste] |
|
24089 | 92 |
\emph{Never} copy-and-paste code when programming. If you |
21148 | 93 |
need the same piece of code twice, introduce a |
94 |
reasonable auxiliary function (if there is no |
|
95 |
such function, very likely you got something wrong). |
|
96 |
Any copy-and-paste will turn out to be painful |
|
97 |
when something has to be changed or fixed later on. |
|
98 |
||
99 |
\item[comments] |
|
100 |
are a device which requires careful thinking before using |
|
101 |
it. The best comment for your code should be the code itself. |
|
102 |
Prefer efforts to write clear, understandable code |
|
103 |
over efforts to explain nasty code. |
|
104 |
||
105 |
\item[functional programming is based on functions] |
|
24089 | 106 |
Avoid ``constructivisms'', i.e.\ unnecessary concrete datatype |
107 |
representations. Instead model things as abstract as |
|
108 |
appropriate. For example, pass a table lookup function rather |
|
109 |
than a concrete table with lookup performed in body. Accustom |
|
110 |
your way of coding to the level of expressiveness a functional |
|
111 |
programming language is giving onto you. |
|
21148 | 112 |
|
113 |
\item[tuples] |
|
114 |
are often in the way. When there is no striking argument |
|
115 |
to tuple function arguments, just write your function curried. |
|
116 |
||
117 |
\item[telling names] |
|
24089 | 118 |
Any name should tell its purpose as exactly as possible, while |
119 |
keeping its length to the absolutely necessary minimum. Always |
|
120 |
give the same name to function arguments which have the same |
|
121 |
meaning. Separate words by underscores (\verb|int_of_string|, not \verb|intOfString|).\footnote{Some |
|
122 |
recent tools for Emacs include special precautions to cope with |
|
123 |
bumpy names in \isa{camelCase}, e.g.\ for improved on-screen |
|
124 |
readability. It is easier to abstain from using such names in the |
|
125 |
first place.} |
|
21148 | 126 |
|
127 |
\end{description}% |
|
18543 | 128 |
\end{isamarkuptext}% |
129 |
\isamarkuptrue% |
|
130 |
% |
|
24089 | 131 |
\isamarkupsection{Thread-safe programming% |
132 |
} |
|
133 |
\isamarkuptrue% |
|
134 |
% |
|
135 |
\begin{isamarkuptext}% |
|
136 |
Recent versions of Poly/ML (5.1 or later) support multithreaded |
|
137 |
execution based on native operating system threads of the |
|
138 |
underlying platform. Thus threads will actually be executed in |
|
139 |
parallel on multi-core systems. A speedup-factor of approximately |
|
140 |
2--4 can be expected for large well-structured Isabelle sessions, |
|
141 |
where theories are organized as a graph with sufficiently many |
|
142 |
independent nodes. |
|
143 |
||
144 |
Threads lack the memory protection of separate processes, but |
|
145 |
operate concurrently on shared heap memory. This has the advantage |
|
146 |
that results of independent computations are immediately available |
|
147 |
to other threads, without requiring explicit communication, |
|
148 |
reloading, or even recoding of data. |
|
149 |
||
150 |
On the other hand, some programming guidelines need to be observed |
|
151 |
in order to make unprotected parallelism work out smoothly. While |
|
152 |
the ML system implementation is responsible to maintain basic |
|
153 |
integrity of the representation of ML values in memory, the |
|
154 |
application programmer needs to ensure that multithreaded execution |
|
155 |
does not break the intended semantics. |
|
156 |
||
157 |
\medskip \paragraph{Critical shared resources.} Actually only those |
|
158 |
parts outside the purely functional world of ML are critical. In |
|
159 |
particular, this covers |
|
160 |
||
161 |
\begin{itemize} |
|
162 |
||
163 |
\item global references (or arrays), i.e.\ those that persist over |
|
164 |
several invocations of associated operations,\footnote{This is |
|
165 |
independent of the visibility of such mutable values in the toplevel |
|
166 |
scope.} |
|
167 |
||
168 |
\item global ML bindings in the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to |
|
169 |
run-time invocation of the compiler, |
|
170 |
||
171 |
\item direct I/O on shared channels, notably \isa{stdin}, \isa{stdout}, \isa{stderr}. |
|
172 |
||
173 |
\end{itemize} |
|
174 |
||
175 |
The majority of tools implemented within the Isabelle/Isar framework |
|
176 |
will not require any of these critical elements: nothing special |
|
177 |
needs to be observed when staying in the purely functional fragment |
|
178 |
of ML. Note that output via the official Isabelle channels does not |
|
179 |
even count as direct I/O in the above sense, so the operations \verb|writeln|, \verb|warning|, \verb|tracing| etc.\ are safe. |
|
180 |
||
181 |
\paragraph{Multithreading in Isabelle/Isar.} Our parallel execution |
|
182 |
model is centered around the theory loader. Whenever a given |
|
183 |
subgraph of theories needs to be updated, the system schedules a |
|
184 |
number of threads to process the sources as required, while |
|
185 |
observing their dependencies. Thus concurrency is limited to |
|
186 |
independent nodes according to the theory import relation. |
|
187 |
||
188 |
Any user-code that works relatively to the present background theory |
|
189 |
is already safe. Contextual data may be easily stored within the |
|
24090 | 190 |
theory or proof context, thanks to the generic data concept of |
191 |
Isabelle/Isar (see \secref{sec:context-data}). This greatly |
|
24089 | 192 |
diminishes the demand for global state information in the first |
193 |
place. |
|
194 |
||
195 |
\medskip In rare situations where actual mutable content needs to be |
|
196 |
manipulated, Isabelle provides a single \emph{critical section} that |
|
197 |
may be entered while preventing any other thread from doing the |
|
198 |
same. Entering the critical section without contention is very |
|
199 |
fast, and several basic system operations do so frequently. This |
|
200 |
also means that each thread should leave the critical section |
|
201 |
quickly, otherwise parallel execution performance may degrade |
|
202 |
significantly. |
|
203 |
||
204 |
Despite this potential bottle-neck, we refrain from fine-grained |
|
205 |
locking mechanisms: the restriction to a single lock prevents |
|
206 |
deadlocks without demanding further considerations in user programs. |
|
207 |
||
208 |
\paragraph{Good conduct of impure programs.} The following |
|
209 |
guidelines enable non-functional programs to participate in |
|
210 |
multithreading. |
|
211 |
||
212 |
\begin{itemize} |
|
213 |
||
214 |
\item Minimize global state information. Using proper theory and |
|
215 |
proof context data will actually return to functional update of |
|
216 |
values, without any special precautions for multithreading. Apart |
|
217 |
from the fully general functors for theory and proof data (see |
|
218 |
\secref{sec:context-data}) there are drop-in replacements that |
|
24090 | 219 |
emulate primitive references for common cases of \emph{configuration |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24090
diff
changeset
|
220 |
options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|Config| and \verb|Attrib.config_bool| etc.), and lists of theorems (see functor |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24090
diff
changeset
|
221 |
\verb|NamedThmsFun|). |
24089 | 222 |
|
223 |
\item Keep components with local state information |
|
224 |
\emph{re-entrant}. Instead of poking initial values into (private) |
|
225 |
global references, create a new state record on each invocation, and |
|
226 |
pass that through any auxiliary functions of the component. The |
|
227 |
state record may well contain mutable references, without requiring |
|
228 |
any special synchronizations, as long as each invocation sees its |
|
229 |
own copy. Occasionally, one might even return to plain functional |
|
230 |
updates on non-mutable record values here. |
|
231 |
||
232 |
\item Isolate process configuration flags. The main legitimate |
|
233 |
application of global references is to configure the whole process |
|
234 |
in a certain way, essentially affecting all threads. A typical |
|
235 |
example is the \verb|show_types| flag, which tells the pretty printer |
|
236 |
to output explicit type information for terms. Such flags usually |
|
237 |
do not affect the functionality of the core system, but only the |
|
24090 | 238 |
view being presented to the user. |
24089 | 239 |
|
240 |
Occasionally, such global process flags are treated like implicit |
|
241 |
arguments to certain operations, by using the \verb|setmp| combinator |
|
24090 | 242 |
for safe temporary assignment. Its traditional purpose was to |
243 |
ensure proper recovery of the original value when exceptions are |
|
244 |
raised in the body, now the functionality is extended to enter the |
|
245 |
\emph{critical section} (with its usual potential of degrading |
|
246 |
parallelism). |
|
24089 | 247 |
|
248 |
Note that recovery of plain value passing semantics via \verb|setmp|~\isa{ref\ value} assumes that this \isa{ref} is |
|
249 |
exclusively manipulated within the critical section. In particular, |
|
250 |
any persistent global assignment of \isa{ref\ {\isacharcolon}{\isacharequal}\ value} needs to |
|
251 |
be marked critical as well, to prevent intruding another threads |
|
252 |
local view, and a lost-update in the global scope, too. |
|
253 |
||
254 |
\item Minimize global ML bindings. Processing theories occasionally |
|
255 |
affects the global ML environment as well. While each ML |
|
256 |
compilation unit is safe, the order of scheduling of independent |
|
257 |
declarations might cause problems when composing several modules |
|
258 |
later on, due to hiding of previous ML names. |
|
259 |
||
260 |
This cannot be helped in general, because the ML toplevel lacks the |
|
261 |
graph structure of the Isabelle theory space. Nevertheless, some |
|
262 |
sound conventions of keeping global ML names essentially disjoint |
|
263 |
(e.g.\ with the help of ML structures) prevents the problem to occur |
|
264 |
in most practical situations. |
|
265 |
||
266 |
\end{itemize} |
|
267 |
||
268 |
Recall that in an open ``LCF-style'' system like Isabelle/Isar, the |
|
269 |
user participates in constructing the overall environment. This |
|
24090 | 270 |
means that state-based facilities offered by one component will |
271 |
require special caution later on. So minimizing critical elements, |
|
272 |
by staying within the plain value-oriented view relative to theory |
|
273 |
or proof contexts most of the time, will also reduce the chance of |
|
24089 | 274 |
mishaps occurring to end-users.% |
275 |
\end{isamarkuptext}% |
|
276 |
\isamarkuptrue% |
|
277 |
% |
|
278 |
\isadelimmlref |
|
279 |
% |
|
280 |
\endisadelimmlref |
|
281 |
% |
|
282 |
\isatagmlref |
|
283 |
% |
|
284 |
\begin{isamarkuptext}% |
|
285 |
\begin{mldecls} |
|
286 |
\indexml{NAMED-CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\ |
|
287 |
\indexml{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\ |
|
288 |
\indexml{setmp}\verb|setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\ |
|
289 |
\end{mldecls} |
|
290 |
||
291 |
\begin{description} |
|
292 |
||
293 |
\item \verb|NAMED_CRITICAL|~\isa{name\ f} evaluates \isa{f\ {\isacharparenleft}{\isacharparenright}} |
|
24090 | 294 |
while staying within the critical section of Isabelle/Isar. No |
295 |
other thread may do so at the same time, but non-critical parallel |
|
296 |
execution will continue. The \isa{name} argument serves for |
|
297 |
diagnostic purposes and might help to spot sources of congestion. |
|
24089 | 298 |
|
299 |
\item \verb|CRITICAL| is the same as \verb|NAMED_CRITICAL| with empty |
|
300 |
name argument. |
|
301 |
||
302 |
\item \verb|setmp|~\isa{ref\ value\ f\ x} evaluates \isa{f\ x} |
|
303 |
while staying within the critical section and having \isa{ref\ {\isacharcolon}{\isacharequal}\ value} assigned temporarily. This recovers a value-passing |
|
304 |
semantics involving global references, regardless of exceptions or |
|
305 |
concurrency. |
|
306 |
||
307 |
\end{description}% |
|
308 |
\end{isamarkuptext}% |
|
309 |
\isamarkuptrue% |
|
310 |
% |
|
311 |
\endisatagmlref |
|
312 |
{\isafoldmlref}% |
|
313 |
% |
|
314 |
\isadelimmlref |
|
315 |
% |
|
316 |
\endisadelimmlref |
|
317 |
% |
|
18543 | 318 |
\isamarkupchapter{Basic library functions% |
319 |
} |
|
320 |
\isamarkuptrue% |
|
321 |
% |
|
322 |
\begin{isamarkuptext}% |
|
22293 | 323 |
Beyond the proposal of the SML/NJ basis library, Isabelle comes |
324 |
with its own library, from which selected parts are given here. |
|
325 |
See further files \emph{Pure/library.ML} and \emph{Pure/General/*.ML}.% |
|
326 |
\end{isamarkuptext}% |
|
327 |
\isamarkuptrue% |
|
328 |
% |
|
329 |
\isamarkupsection{Linear transformations% |
|
330 |
} |
|
331 |
\isamarkuptrue% |
|
332 |
% |
|
333 |
\isadelimmlref |
|
334 |
% |
|
335 |
\endisadelimmlref |
|
336 |
% |
|
337 |
\isatagmlref |
|
338 |
% |
|
339 |
\begin{isamarkuptext}% |
|
340 |
\begin{mldecls} |
|
24089 | 341 |
\indexml{op |$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\ |
22293 | 342 |
\end{mldecls}% |
343 |
\end{isamarkuptext}% |
|
344 |
\isamarkuptrue% |
|
345 |
% |
|
346 |
\endisatagmlref |
|
347 |
{\isafoldmlref}% |
|
348 |
% |
|
349 |
\isadelimmlref |
|
350 |
% |
|
351 |
\endisadelimmlref |
|
352 |
% |
|
22322 | 353 |
\isadelimML |
354 |
% |
|
355 |
\endisadelimML |
|
356 |
% |
|
357 |
\isatagML |
|
358 |
% |
|
359 |
\endisatagML |
|
360 |
{\isafoldML}% |
|
361 |
% |
|
362 |
\isadelimML |
|
363 |
% |
|
364 |
\endisadelimML |
|
365 |
% |
|
22293 | 366 |
\begin{isamarkuptext}% |
22322 | 367 |
Many problems in functional programming can be thought of |
368 |
as linear transformations, i.e.~a caluclation starts with a |
|
369 |
particular value \isa{x\ {\isasymColon}\ foo} which is then transformed |
|
370 |
by application of a function \isa{f\ {\isasymColon}\ foo\ {\isasymRightarrow}\ foo}, |
|
371 |
continued by an application of a function \isa{g\ {\isasymColon}\ foo\ {\isasymRightarrow}\ bar}, |
|
25151 | 372 |
and so on. As a canoncial example, take functions enriching |
373 |
a theory by constant declararion and primitive definitions: |
|
374 |
||
375 |
\begin{quotation} |
|
376 |
\verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix|\isasep\isanewline% |
|
377 |
\verb| -> theory -> term * theory| |
|
378 |
||
25608 | 379 |
\verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory| |
25151 | 380 |
\end{quotation} |
381 |
||
382 |
Written with naive application, an addition of constant |
|
383 |
\isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and |
|
384 |
a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like: |
|
385 |
||
386 |
\begin{quotation} |
|
25608 | 387 |
\verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline% |
25151 | 388 |
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline% |
389 |
\verb| (Sign.declare_const []|\isasep\isanewline% |
|
25185 | 390 |
\verb| ("bar", @{typ "foo => foo"}, NoSyn) thy)| |
25151 | 391 |
\end{quotation} |
392 |
||
393 |
With increasing numbers of applications, this code gets quite |
|
394 |
unreadable. Further, it is unintuitive that things are |
|
395 |
written down in the opposite order as they actually ``happen''.% |
|
22322 | 396 |
\end{isamarkuptext}% |
397 |
\isamarkuptrue% |
|
398 |
% |
|
399 |
\begin{isamarkuptext}% |
|
25151 | 400 |
\noindent At this stage, Isabelle offers some combinators which allow |
401 |
for more convenient notation, most notably reverse application: |
|
402 |
\begin{quotation} |
|
22322 | 403 |
\verb|thy|\isasep\isanewline% |
25151 | 404 |
\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
405 |
\verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline% |
|
25608 | 406 |
\verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline% |
25151 | 407 |
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))| |
408 |
\end{quotation}% |
|
22293 | 409 |
\end{isamarkuptext}% |
410 |
\isamarkuptrue% |
|
411 |
% |
|
412 |
\isadelimmlref |
|
413 |
% |
|
414 |
\endisadelimmlref |
|
415 |
% |
|
416 |
\isatagmlref |
|
417 |
% |
|
418 |
\begin{isamarkuptext}% |
|
419 |
\begin{mldecls} |
|
24089 | 420 |
\indexml{op |-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\ |
421 |
\indexml{op |$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\ |
|
422 |
\indexml{op ||$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\ |
|
423 |
\indexml{op ||$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\ |
|
25151 | 424 |
\end{mldecls}% |
425 |
\end{isamarkuptext}% |
|
426 |
\isamarkuptrue% |
|
427 |
% |
|
428 |
\endisatagmlref |
|
429 |
{\isafoldmlref}% |
|
430 |
% |
|
431 |
\isadelimmlref |
|
432 |
% |
|
433 |
\endisadelimmlref |
|
434 |
% |
|
435 |
\begin{isamarkuptext}% |
|
436 |
\noindent Usually, functions involving theory updates also return |
|
437 |
side results; to use these conveniently, yet another |
|
438 |
set of combinators is at hand, most notably \verb|op |\verb,|,\verb|->| |
|
439 |
which allows curried access to side results: |
|
440 |
\begin{quotation} |
|
441 |
\verb|thy|\isasep\isanewline% |
|
442 |
\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
|
25608 | 443 |
\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline% |
25151 | 444 |
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline% |
445 |
||
446 |
\end{quotation} |
|
447 |
||
448 |
\noindent \verb|op |\verb,|,\verb|>>| allows for processing side results on their own: |
|
449 |
\begin{quotation} |
|
450 |
\verb|thy|\isasep\isanewline% |
|
451 |
\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
|
452 |
\verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline% |
|
25608 | 453 |
\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false ("bar_def", def))|\isasep\isanewline% |
25151 | 454 |
|
455 |
\end{quotation} |
|
456 |
||
457 |
\noindent Orthogonally, \verb|op |\verb,|,\verb||\verb,|,\verb|>| applies a transformation |
|
458 |
in the presence of side results which are left unchanged: |
|
459 |
\begin{quotation} |
|
460 |
\verb|thy|\isasep\isanewline% |
|
461 |
\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
|
462 |
\verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline% |
|
25608 | 463 |
\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline% |
25151 | 464 |
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline% |
465 |
\verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline% |
|
466 |
||
467 |
\end{quotation} |
|
468 |
||
469 |
\noindent \indexml{op ||$>$$>$}\verb|op |\verb,|,\verb||\verb,|,\verb|>>| accumulates side results: |
|
470 |
\begin{quotation} |
|
471 |
\verb|thy|\isasep\isanewline% |
|
472 |
\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
|
473 |
\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ("foobar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
|
25608 | 474 |
\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline% |
25151 | 475 |
\verb| ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline% |
476 |
||
477 |
\end{quotation}% |
|
478 |
\end{isamarkuptext}% |
|
479 |
\isamarkuptrue% |
|
480 |
% |
|
481 |
\isadelimmlref |
|
482 |
% |
|
483 |
\endisadelimmlref |
|
484 |
% |
|
485 |
\isatagmlref |
|
486 |
% |
|
487 |
\begin{isamarkuptext}% |
|
488 |
\begin{mldecls} |
|
489 |
\indexml{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\ |
|
22293 | 490 |
\indexml{fold-map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\ |
491 |
\end{mldecls}% |
|
492 |
\end{isamarkuptext}% |
|
493 |
\isamarkuptrue% |
|
494 |
% |
|
22322 | 495 |
\endisatagmlref |
496 |
{\isafoldmlref}% |
|
497 |
% |
|
498 |
\isadelimmlref |
|
499 |
% |
|
500 |
\endisadelimmlref |
|
501 |
% |
|
502 |
\begin{isamarkuptext}% |
|
25151 | 503 |
\noindent This principles naturally lift to \isa{lists} using |
504 |
the \verb|fold| and \verb|fold_map| combinators. |
|
505 |
The first lifts a single function |
|
25185 | 506 |
\[ |
507 |
\mbox{\isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}} |
|
508 |
\] |
|
25151 | 509 |
such that |
25185 | 510 |
\[ |
511 |
\mbox{\isa{y\ {\isacharbar}{\isachargreater}\ fold\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub n}} |
|
512 |
\] |
|
513 |
The second accumulates side results in a list by lifting |
|
25151 | 514 |
a single function |
25185 | 515 |
\[ |
516 |
\mbox{\isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ list\ {\isasymtimes}\ {\isacharprime}b}} |
|
517 |
\] |
|
25151 | 518 |
such that |
25185 | 519 |
\[ |
520 |
\mbox{\isa{y\ {\isacharbar}{\isachargreater}\ fold{\isacharunderscore}map\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}}} \\ |
|
521 |
~~\mbox{\isa{y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub n\ {\isacharbar}{\isacharbar}{\isachargreater}\ {\isacharparenleft}fn\ {\isacharparenleft}{\isacharparenleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharparenright}\ {\isacharequal}{\isachargreater}\ {\isacharbrackleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharbrackright}{\isacharparenright}}} |
|
522 |
\] |
|
523 |
||
524 |
Example: |
|
525 |
\begin{quotation} |
|
526 |
\verb|let|\isasep\isanewline% |
|
527 |
\verb| val consts = ["foo", "bar"];|\isasep\isanewline% |
|
528 |
\verb|in|\isasep\isanewline% |
|
529 |
\verb| thy|\isasep\isanewline% |
|
530 |
\verb| |\verb,|,\verb|> fold_map (fn const => Sign.declare_const []|\isasep\isanewline% |
|
531 |
\verb| (const, @{typ "foo => foo"}, NoSyn)) consts|\isasep\isanewline% |
|
532 |
\verb| |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline% |
|
533 |
\verb| |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline% |
|
25608 | 534 |
\verb| Thm.add_def false false ("", def)) defs)|\isasep\isanewline% |
25185 | 535 |
\verb|end|\isasep\isanewline% |
25151 | 536 |
|
537 |
\end{quotation}% |
|
22322 | 538 |
\end{isamarkuptext}% |
539 |
\isamarkuptrue% |
|
540 |
% |
|
541 |
\isadelimmlref |
|
542 |
% |
|
543 |
\endisadelimmlref |
|
544 |
% |
|
545 |
\isatagmlref |
|
546 |
% |
|
22293 | 547 |
\begin{isamarkuptext}% |
548 |
\begin{mldecls} |
|
24089 | 549 |
\indexml{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\ |
550 |
\indexml{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\ |
|
551 |
\indexml{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\ |
|
552 |
\indexml{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\ |
|
553 |
\indexml{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\ |
|
22293 | 554 |
\end{mldecls}% |
555 |
\end{isamarkuptext}% |
|
556 |
\isamarkuptrue% |
|
557 |
% |
|
22322 | 558 |
\endisatagmlref |
559 |
{\isafoldmlref}% |
|
560 |
% |
|
561 |
\isadelimmlref |
|
562 |
% |
|
563 |
\endisadelimmlref |
|
564 |
% |
|
565 |
\begin{isamarkuptext}% |
|
22550 | 566 |
\noindent All those linear combinators also exist in higher-order |
567 |
variants which do not expect a value on the left hand side |
|
568 |
but a function.% |
|
22322 | 569 |
\end{isamarkuptext}% |
570 |
\isamarkuptrue% |
|
571 |
% |
|
572 |
\isadelimmlref |
|
573 |
% |
|
574 |
\endisadelimmlref |
|
575 |
% |
|
576 |
\isatagmlref |
|
577 |
% |
|
22293 | 578 |
\begin{isamarkuptext}% |
579 |
\begin{mldecls} |
|
24089 | 580 |
\indexml{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\ |
22293 | 581 |
\indexml{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\ |
582 |
\end{mldecls}% |
|
583 |
\end{isamarkuptext}% |
|
584 |
\isamarkuptrue% |
|
585 |
% |
|
586 |
\endisatagmlref |
|
587 |
{\isafoldmlref}% |
|
588 |
% |
|
589 |
\isadelimmlref |
|
590 |
% |
|
591 |
\endisadelimmlref |
|
592 |
% |
|
22550 | 593 |
\begin{isamarkuptext}% |
25185 | 594 |
\noindent These operators allow to ``query'' a context |
595 |
in a series of context transformations: |
|
596 |
||
597 |
\begin{quotation} |
|
598 |
\verb|thy|\isasep\isanewline% |
|
599 |
\verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline% |
|
600 |
\verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline% |
|
601 |
\verb||\verb,|,\verb||\verb,|,\verb|>> `(fn thy => Sign.declared_const thy|\isasep\isanewline% |
|
602 |
\verb| (Sign.full_name thy "foobar"))|\isasep\isanewline% |
|
603 |
\verb||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline% |
|
604 |
\verb| else Sign.declare_const []|\isasep\isanewline% |
|
605 |
\verb| ("foobar", @{typ "foo => foo"}, NoSyn) #> snd)|\isasep\isanewline% |
|
606 |
||
607 |
\end{quotation}% |
|
22550 | 608 |
\end{isamarkuptext}% |
609 |
\isamarkuptrue% |
|
610 |
% |
|
22293 | 611 |
\isamarkupsection{Options and partiality% |
612 |
} |
|
613 |
\isamarkuptrue% |
|
614 |
% |
|
615 |
\isadelimmlref |
|
616 |
% |
|
617 |
\endisadelimmlref |
|
618 |
% |
|
619 |
\isatagmlref |
|
620 |
% |
|
621 |
\begin{isamarkuptext}% |
|
622 |
\begin{mldecls} |
|
623 |
\indexml{is-some}\verb|is_some: 'a option -> bool| \\ |
|
624 |
\indexml{is-none}\verb|is_none: 'a option -> bool| \\ |
|
625 |
\indexml{the}\verb|the: 'a option -> 'a| \\ |
|
626 |
\indexml{these}\verb|these: 'a list option -> 'a list| \\ |
|
627 |
\indexml{the-list}\verb|the_list: 'a option -> 'a list| \\ |
|
628 |
\indexml{the-default}\verb|the_default: 'a -> 'a option -> 'a| \\ |
|
629 |
\indexml{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\ |
|
630 |
\indexml{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\ |
|
631 |
\end{mldecls}% |
|
632 |
\end{isamarkuptext}% |
|
633 |
\isamarkuptrue% |
|
634 |
% |
|
635 |
\endisatagmlref |
|
636 |
{\isafoldmlref}% |
|
637 |
% |
|
638 |
\isadelimmlref |
|
639 |
% |
|
640 |
\endisadelimmlref |
|
641 |
% |
|
642 |
\begin{isamarkuptext}% |
|
24089 | 643 |
Standard selector functions on \isa{option}s are provided. The |
644 |
\verb|try| and \verb|can| functions provide a convenient interface for |
|
645 |
handling exceptions -- both take as arguments a function \isa{f} |
|
646 |
together with a parameter \isa{x} and handle any exception during |
|
647 |
the evaluation of the application of \isa{f} to \isa{x}, either |
|
648 |
return a lifted result (\verb|NONE| on failure) or a boolean value |
|
649 |
(\verb|false| on failure).% |
|
22293 | 650 |
\end{isamarkuptext}% |
651 |
\isamarkuptrue% |
|
652 |
% |
|
653 |
\isamarkupsection{Common data structures% |
|
654 |
} |
|
655 |
\isamarkuptrue% |
|
656 |
% |
|
657 |
\isamarkupsubsection{Lists (as set-like data structures)% |
|
658 |
} |
|
659 |
\isamarkuptrue% |
|
660 |
% |
|
661 |
\begin{isamarkuptext}% |
|
662 |
\begin{mldecls} |
|
663 |
\indexml{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\ |
|
664 |
\indexml{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\ |
|
665 |
\indexml{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\ |
|
666 |
\indexml{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\ |
|
667 |
\end{mldecls}% |
|
668 |
\end{isamarkuptext}% |
|
669 |
\isamarkuptrue% |
|
670 |
% |
|
671 |
\begin{isamarkuptext}% |
|
22503 | 672 |
Lists are often used as set-like data structures -- set-like in |
25151 | 673 |
the sense that they support a notion of \verb|member|-ship, |
22503 | 674 |
\verb|insert|-ing and \verb|remove|-ing, but are order-sensitive. |
675 |
This is convenient when implementing a history-like mechanism: |
|
676 |
\verb|insert| adds an element \emph{to the front} of a list, |
|
677 |
if not yet present; \verb|remove| removes \emph{all} occurences |
|
678 |
of a particular element. Correspondingly \verb|merge| implements a |
|
679 |
a merge on two lists suitable for merges of context data |
|
680 |
(\secref{sec:context-theory}). |
|
681 |
||
682 |
Functions are parametrized by an explicit equality function |
|
683 |
to accomplish overloaded equality; in most cases of monomorphic |
|
24089 | 684 |
equality, writing \verb|op =| should suffice.% |
22293 | 685 |
\end{isamarkuptext}% |
686 |
\isamarkuptrue% |
|
687 |
% |
|
688 |
\isamarkupsubsection{Association lists% |
|
689 |
} |
|
690 |
\isamarkuptrue% |
|
691 |
% |
|
692 |
\begin{isamarkuptext}% |
|
693 |
\begin{mldecls} |
|
694 |
\indexmlexception{AList.DUP}\verb|exception AList.DUP| \\ |
|
695 |
\indexml{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\ |
|
696 |
\indexml{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\ |
|
697 |
\indexml{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\ |
|
698 |
\indexml{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\ |
|
699 |
\indexml{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\ |
|
700 |
\indexml{AList.map-entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline% |
|
701 |
\verb| -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\ |
|
702 |
\indexml{AList.map-default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline% |
|
703 |
\verb| -> ('a * 'b) list -> ('a * 'b) list| \\ |
|
704 |
\indexml{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline% |
|
705 |
\verb| -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| \\ |
|
706 |
\indexml{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline% |
|
707 |
\verb| -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| |
|
708 |
\end{mldecls}% |
|
709 |
\end{isamarkuptext}% |
|
710 |
\isamarkuptrue% |
|
711 |
% |
|
712 |
\begin{isamarkuptext}% |
|
22503 | 713 |
Association lists can be seens as an extension of set-like lists: |
714 |
on the one hand, they may be used to implement finite mappings, |
|
715 |
on the other hand, they remain order-sensitive and allow for |
|
716 |
multiple key-value-pair with the same key: \verb|AList.lookup| |
|
717 |
returns the \emph{first} value corresponding to a particular |
|
718 |
key, if present. \verb|AList.update| updates |
|
719 |
the \emph{first} occurence of a particular key; if no such |
|
720 |
key exists yet, the key-value-pair is added \emph{to the front}. |
|
721 |
\verb|AList.delete| only deletes the \emph{first} occurence of a key. |
|
722 |
\verb|AList.merge| provides an operation suitable for merges of context data |
|
723 |
(\secref{sec:context-theory}), where an equality parameter on |
|
724 |
values determines whether a merge should be considered a conflict. |
|
725 |
A slightly generalized operation if implementend by the \verb|AList.join| |
|
726 |
function which allows for explicit conflict resolution.% |
|
22293 | 727 |
\end{isamarkuptext}% |
728 |
\isamarkuptrue% |
|
729 |
% |
|
730 |
\isamarkupsubsection{Tables% |
|
731 |
} |
|
732 |
\isamarkuptrue% |
|
733 |
% |
|
734 |
\begin{isamarkuptext}% |
|
735 |
\begin{mldecls} |
|
736 |
\indexmltype{'a Symtab.table}\verb|type 'a Symtab.table| \\ |
|
23653 | 737 |
\indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of string| \\ |
22293 | 738 |
\indexmlexception{Symtab.SAME}\verb|exception Symtab.SAME| \\ |
23653 | 739 |
\indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\ |
22293 | 740 |
\indexml{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\ |
23653 | 741 |
\indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\ |
742 |
\indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\ |
|
743 |
\indexml{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\ |
|
744 |
\indexml{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\ |
|
745 |
\indexml{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline% |
|
22293 | 746 |
\verb| -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\ |
23653 | 747 |
\indexml{Symtab.map-entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline% |
22293 | 748 |
\verb| -> 'a Symtab.table -> 'a Symtab.table| \\ |
23653 | 749 |
\indexml{Symtab.map-default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline% |
22293 | 750 |
\verb| -> 'a Symtab.table -> 'a Symtab.table| \\ |
23653 | 751 |
\indexml{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline% |
22293 | 752 |
\verb| -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline% |
23653 | 753 |
\verb| -> 'a Symtab.table (*exception Symtab.DUP*)| \\ |
22293 | 754 |
\indexml{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline% |
755 |
\verb| -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline% |
|
23653 | 756 |
\verb| -> 'a Symtab.table (*exception Symtab.DUP*)| |
22293 | 757 |
\end{mldecls}% |
758 |
\end{isamarkuptext}% |
|
759 |
\isamarkuptrue% |
|
760 |
% |
|
761 |
\begin{isamarkuptext}% |
|
22503 | 762 |
Tables are an efficient representation of finite mappings without |
763 |
any notion of order; due to their efficiency they should be used |
|
764 |
whenever such pure finite mappings are neccessary. |
|
765 |
||
766 |
The key type of tables must be given explicitly by instantiating |
|
767 |
the \verb|TableFun| functor which takes the key type |
|
768 |
together with its \verb|order|; for convience, we restrict |
|
769 |
here to the \verb|Symtab| instance with \verb|string| |
|
770 |
as key type. |
|
771 |
||
772 |
Most table functions correspond to those of association lists.% |
|
18543 | 773 |
\end{isamarkuptext}% |
774 |
\isamarkuptrue% |
|
775 |
% |
|
20490 | 776 |
\isamarkupchapter{Cookbook% |
777 |
} |
|
778 |
\isamarkuptrue% |
|
779 |
% |
|
20491 | 780 |
\isamarkupsection{A method that depends on declarations in the context% |
20490 | 781 |
} |
782 |
\isamarkuptrue% |
|
783 |
% |
|
784 |
\begin{isamarkuptext}% |
|
785 |
FIXME% |
|
786 |
\end{isamarkuptext}% |
|
787 |
\isamarkuptrue% |
|
788 |
% |
|
18543 | 789 |
\isadelimtheory |
790 |
% |
|
791 |
\endisadelimtheory |
|
792 |
% |
|
793 |
\isatagtheory |
|
794 |
\isacommand{end}\isamarkupfalse% |
|
18537 | 795 |
% |
796 |
\endisatagtheory |
|
797 |
{\isafoldtheory}% |
|
798 |
% |
|
799 |
\isadelimtheory |
|
800 |
% |
|
801 |
\endisadelimtheory |
|
18543 | 802 |
\isanewline |
18537 | 803 |
\end{isabellebody}% |
804 |
%%% Local Variables: |
|
805 |
%%% mode: latex |
|
806 |
%%% TeX-master: "root" |
|
807 |
%%% End: |