1 theory Misc |
|
2 imports Base |
|
3 begin |
|
4 |
|
5 chapter {* Miscellaneous tools \label{ch:tools} *} |
|
6 |
|
7 text {* |
|
8 Subsequently we describe various Isabelle related utilities, given |
|
9 in alphabetical order. |
|
10 *} |
|
11 |
|
12 |
|
13 section {* Resolving Isabelle components \label{sec:tool-components} *} |
|
14 |
|
15 text {* |
|
16 The @{tool_def components} tool resolves Isabelle components: |
|
17 \begin{ttbox} |
|
18 Usage: isabelle components [OPTIONS] [COMPONENTS ...] |
|
19 |
|
20 Options are: |
|
21 -R URL component repository |
|
22 (default $ISABELLE_COMPONENT_REPOSITORY) |
|
23 -a all missing components |
|
24 -l list status |
|
25 |
|
26 Resolve Isabelle components via download and installation. |
|
27 COMPONENTS are identified via base name. |
|
28 |
|
29 ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components" |
|
30 \end{ttbox} |
|
31 |
|
32 Components are initialized as described in \secref{sec:components} |
|
33 in a permissive manner, which can mark components as ``missing''. |
|
34 This state is amended by letting @{tool "components"} download and |
|
35 unpack components that are published on the default component |
|
36 repository \url{http://isabelle.in.tum.de/components/} in |
|
37 particular. |
|
38 |
|
39 Option @{verbatim "-R"} specifies an alternative component |
|
40 repository. Note that @{verbatim "file:///"} URLs can be used for |
|
41 local directories. |
|
42 |
|
43 Option @{verbatim "-a"} selects all missing components to be |
|
44 installed. Explicit components may be named as command |
|
45 line-arguments as well. Note that components are uniquely |
|
46 identified by their base name, while the installation takes place in |
|
47 the location that was specified in the attempt to initialize the |
|
48 component before. |
|
49 |
|
50 Option @{verbatim "-l"} lists the current state of available and |
|
51 missing components with their location (full name) within the |
|
52 file-system. *} |
|
53 |
|
54 |
|
55 section {* Displaying documents *} |
|
56 |
|
57 text {* The @{tool_def display} tool displays documents in DVI or PDF |
|
58 format: |
|
59 \begin{ttbox} |
|
60 Usage: isabelle display [OPTIONS] FILE |
|
61 |
|
62 Options are: |
|
63 -c cleanup -- remove FILE after use |
|
64 |
|
65 Display document FILE (in DVI format). |
|
66 \end{ttbox} |
|
67 |
|
68 \medskip The @{verbatim "-c"} option causes the input file to be |
|
69 removed after use. The program for viewing @{verbatim dvi} files is |
|
70 determined by the @{setting DVI_VIEWER} setting. |
|
71 *} |
|
72 |
|
73 |
|
74 section {* Viewing documentation \label{sec:tool-doc} *} |
|
75 |
|
76 text {* |
|
77 The @{tool_def doc} tool displays online documentation: |
|
78 \begin{ttbox} |
|
79 Usage: isabelle doc [DOC] |
|
80 |
|
81 View Isabelle documentation DOC, or show list of available documents. |
|
82 \end{ttbox} |
|
83 If called without arguments, it lists all available documents. Each |
|
84 line starts with an identifier, followed by a short description. Any |
|
85 of these identifiers may be specified as the first argument in order |
|
86 to have the corresponding document displayed. |
|
87 |
|
88 \medskip The @{setting ISABELLE_DOCS} setting specifies the list of |
|
89 directories (separated by colons) to be scanned for documentations. |
|
90 The program for viewing @{verbatim dvi} files is determined by the |
|
91 @{setting DVI_VIEWER} setting. |
|
92 *} |
|
93 |
|
94 |
|
95 section {* Shell commands within the settings environment \label{sec:tool-env} *} |
|
96 |
|
97 text {* The @{tool_def env} tool is a direct wrapper for the standard |
|
98 @{verbatim "/usr/bin/env"} command on POSIX systems, running within |
|
99 the Isabelle settings environment (\secref{sec:settings}). |
|
100 |
|
101 The command-line arguments are that of the underlying version of |
|
102 @{verbatim env}. For example, the following invokes an instance of |
|
103 the GNU Bash shell within the Isabelle environment: |
|
104 \begin{alltt} |
|
105 isabelle env bash |
|
106 \end{alltt} |
|
107 *} |
|
108 |
|
109 |
|
110 section {* Getting logic images *} |
|
111 |
|
112 text {* The @{tool_def findlogics} tool traverses all directories |
|
113 specified in @{setting ISABELLE_PATH}, looking for Isabelle logic |
|
114 images. Its usage is: |
|
115 \begin{ttbox} |
|
116 Usage: isabelle findlogics |
|
117 |
|
118 Collect heap file names from ISABELLE_PATH. |
|
119 \end{ttbox} |
|
120 |
|
121 The base names of all files found on the path are printed --- sorted |
|
122 and with duplicates removed. Also note that lookup in @{setting |
|
123 ISABELLE_PATH} includes the current values of @{setting ML_SYSTEM} |
|
124 and @{setting ML_PLATFORM}. Thus switching to another ML compiler |
|
125 may change the set of logic images available. |
|
126 *} |
|
127 |
|
128 |
|
129 section {* Inspecting the settings environment \label{sec:tool-getenv} *} |
|
130 |
|
131 text {* The Isabelle settings environment --- as provided by the |
|
132 site-default and user-specific settings files --- can be inspected |
|
133 with the @{tool_def getenv} tool: |
|
134 \begin{ttbox} |
|
135 Usage: isabelle getenv [OPTIONS] [VARNAMES ...] |
|
136 |
|
137 Options are: |
|
138 -a display complete environment |
|
139 -b print values only (doesn't work for -a) |
|
140 -d FILE dump complete environment to FILE |
|
141 (null terminated entries) |
|
142 |
|
143 Get value of VARNAMES from the Isabelle settings. |
|
144 \end{ttbox} |
|
145 |
|
146 With the @{verbatim "-a"} option, one may inspect the full process |
|
147 environment that Isabelle related programs are run in. This usually |
|
148 contains much more variables than are actually Isabelle settings. |
|
149 Normally, output is a list of lines of the form @{text |
|
150 name}@{verbatim "="}@{text value}. The @{verbatim "-b"} option |
|
151 causes only the values to be printed. |
|
152 |
|
153 Option @{verbatim "-d"} produces a dump of the complete environment |
|
154 to the specified file. Entries are terminated by the ASCII null |
|
155 character, i.e.\ the C string terminator. |
|
156 *} |
|
157 |
|
158 |
|
159 subsubsection {* Examples *} |
|
160 |
|
161 text {* Get the location of @{setting ISABELLE_HOME_USER} where |
|
162 user-specific information is stored: |
|
163 \begin{ttbox} |
|
164 isabelle getenv ISABELLE_HOME_USER |
|
165 \end{ttbox} |
|
166 |
|
167 \medskip Get the value only of the same settings variable, which is |
|
168 particularly useful in shell scripts: |
|
169 \begin{ttbox} |
|
170 isabelle getenv -b ISABELLE_OUTPUT |
|
171 \end{ttbox} |
|
172 *} |
|
173 |
|
174 |
|
175 section {* Installing standalone Isabelle executables \label{sec:tool-install} *} |
|
176 |
|
177 text {* By default, the main Isabelle binaries (@{executable |
|
178 "isabelle"} etc.) are just run from their location within the |
|
179 distribution directory, probably indirectly by the shell through its |
|
180 @{setting PATH}. Other schemes of installation are supported by the |
|
181 @{tool_def install} tool: |
|
182 \begin{ttbox} |
|
183 Usage: isabelle install [OPTIONS] |
|
184 |
|
185 Options are: |
|
186 -d DISTDIR use DISTDIR as Isabelle distribution |
|
187 (default ISABELLE_HOME) |
|
188 -p DIR install standalone binaries in DIR |
|
189 |
|
190 Install Isabelle executables with absolute references to the current |
|
191 distribution directory. |
|
192 \end{ttbox} |
|
193 |
|
194 The @{verbatim "-d"} option overrides the current Isabelle |
|
195 distribution directory as determined by @{setting ISABELLE_HOME}. |
|
196 |
|
197 The @{verbatim "-p"} option installs executable wrapper scripts for |
|
198 @{executable "isabelle-process"}, @{executable isabelle}, containing |
|
199 proper absolute references to the Isabelle distribution directory. |
|
200 A typical @{verbatim DIR} specification would be some directory |
|
201 expected to be in the shell's @{setting PATH}, such as @{verbatim |
|
202 "$HOME/bin"}. |
|
203 |
|
204 It is possible to make symbolic links of the main Isabelle |
|
205 executables, but making separate copies outside the Isabelle |
|
206 distribution directory will not work. |
|
207 *} |
|
208 |
|
209 |
|
210 section {* Creating instances of the Isabelle logo *} |
|
211 |
|
212 text {* The @{tool_def logo} tool creates any instance of the generic |
|
213 Isabelle logo as EPS or PDF. |
|
214 \begin{ttbox} |
|
215 Usage: isabelle logo [OPTIONS] NAME |
|
216 |
|
217 Create instance NAME of the Isabelle logo (as EPS or PDF). |
|
218 |
|
219 Options are: |
|
220 -o OUTFILE specify output file and format |
|
221 (default "isabelle_name.pdf") |
|
222 -q quiet mode |
|
223 \end{ttbox} |
|
224 |
|
225 Option @{verbatim "-o"} specifies an explicit output file name and |
|
226 format, e.g.\ @{verbatim "mylogo.eps"} for an EPS logo. The default |
|
227 is @{verbatim "isabelle_"}@{text name}@{verbatim ".pdf"}, with the |
|
228 lower-case version of the given name and PDF output. |
|
229 |
|
230 Option @{verbatim "-q"} omits printing of the result file name. |
|
231 |
|
232 \medskip Implementors of Isabelle tools and applications are |
|
233 encouraged to make derived Isabelle logos for their own projects |
|
234 using this template. *} |
|
235 |
|
236 |
|
237 section {* Isabelle wrapper for make \label{sec:tool-make} *} |
|
238 |
|
239 text {* The old @{tool_def make} tool is a very simple wrapper for |
|
240 ordinary Unix @{executable make}: |
|
241 \begin{ttbox} |
|
242 Usage: isabelle make [ARGS ...] |
|
243 |
|
244 Compile the logic in current directory using IsaMakefile. |
|
245 ARGS are directly passed to the system make program. |
|
246 \end{ttbox} |
|
247 |
|
248 Note that the Isabelle settings environment is also active. Thus one |
|
249 may refer to its values within the @{verbatim IsaMakefile}, e.g.\ |
|
250 @{verbatim "$(ISABELLE_HOME)"}. Furthermore, programs started from |
|
251 the make file also inherit this environment. |
|
252 *} |
|
253 |
|
254 |
|
255 section {* Creating Isabelle session directories |
|
256 \label{sec:tool-mkdir} *} |
|
257 |
|
258 text {* The old @{tool_def mkdir} tool prepares Isabelle session |
|
259 source directories, including a sensible default setup of @{verbatim |
|
260 IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document} |
|
261 directory with a minimal @{verbatim root.tex} that is sufficient to |
|
262 print all theories of the session (in the order of appearance); see |
|
263 \secref{sec:tool-document} for further information on Isabelle |
|
264 document preparation. The usage of @{tool mkdir} is: |
|
265 |
|
266 \begin{ttbox} |
|
267 Usage: isabelle mkdir [OPTIONS] [LOGIC] NAME |
|
268 |
|
269 Options are: |
|
270 -I FILE alternative IsaMakefile output |
|
271 -P include parent logic target |
|
272 -b setup build mode (session outputs heap image) |
|
273 -q quiet mode |
|
274 |
|
275 Prepare session directory, including IsaMakefile and document source, |
|
276 with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC) |
|
277 \end{ttbox} |
|
278 |
|
279 The @{tool mkdir} tool is conservative in the sense that any |
|
280 existing @{verbatim IsaMakefile} etc.\ is left unchanged. Thus it |
|
281 is safe to invoke it multiple times, although later runs may not |
|
282 have the desired effect. |
|
283 |
|
284 Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile} |
|
285 incrementally --- manual changes are required for multiple |
|
286 sub-sessions. On order to get an initial working session, the only |
|
287 editing needed is to add appropriate @{ML use_thy} calls to the |
|
288 generated @{verbatim ROOT.ML} file. |
|
289 *} |
|
290 |
|
291 |
|
292 subsubsection {* Options *} |
|
293 |
|
294 text {* |
|
295 The @{verbatim "-I"} option specifies an alternative to @{verbatim |
|
296 IsaMakefile} for dependencies. Note that ``@{verbatim "-"}'' refers |
|
297 to \emph{stdout}, i.e.\ ``@{verbatim "-I-"}'' provides an easy way |
|
298 to peek at @{tool mkdir}'s idea of @{tool make} setup required for |
|
299 some particular of Isabelle session. |
|
300 |
|
301 \medskip The @{verbatim "-P"} option includes a target for the |
|
302 parent @{verbatim LOGIC} session in the generated @{verbatim |
|
303 IsaMakefile}. The corresponding sources are assumed to be located |
|
304 within the Isabelle distribution. |
|
305 |
|
306 \medskip The @{verbatim "-b"} option sets up the current directory |
|
307 as the base for a new session that provides an actual logic image, |
|
308 as opposed to one that only runs several theories based on an |
|
309 existing image. Note that in the latter case, everything except |
|
310 @{verbatim IsaMakefile} would be placed into a separate directory |
|
311 @{verbatim NAME}, rather than the current one. See |
|
312 \secref{sec:tool-usedir} for further information on \emph{build |
|
313 mode} vs.\ \emph{example mode} of @{tool usedir}. |
|
314 |
|
315 \medskip The @{verbatim "-q"} option enables quiet mode, suppressing |
|
316 further notes on how to proceed. |
|
317 *} |
|
318 |
|
319 |
|
320 section {* Printing documents *} |
|
321 |
|
322 text {* |
|
323 The @{tool_def print} tool prints documents: |
|
324 \begin{ttbox} |
|
325 Usage: isabelle print [OPTIONS] FILE |
|
326 |
|
327 Options are: |
|
328 -c cleanup -- remove FILE after use |
|
329 |
|
330 Print document FILE. |
|
331 \end{ttbox} |
|
332 |
|
333 The @{verbatim "-c"} option causes the input file to be removed |
|
334 after use. The printer spool command is determined by the @{setting |
|
335 PRINT_COMMAND} setting. |
|
336 *} |
|
337 |
|
338 |
|
339 section {* Remove awkward symbol names from theory sources *} |
|
340 |
|
341 text {* |
|
342 The @{tool_def unsymbolize} tool tunes Isabelle theory sources to |
|
343 improve readability for plain ASCII output (e.g.\ in email |
|
344 communication). Most notably, @{tool unsymbolize} replaces awkward |
|
345 arrow symbols such as @{verbatim "\\"}@{verbatim "<Longrightarrow>"} |
|
346 by @{verbatim "==>"}. |
|
347 \begin{ttbox} |
|
348 Usage: isabelle unsymbolize [FILES|DIRS...] |
|
349 |
|
350 Recursively find .thy/.ML files, removing unreadable symbol names. |
|
351 Note: this is an ad-hoc script; there is no systematic way to replace |
|
352 symbols independently of the inner syntax of a theory! |
|
353 |
|
354 Renames old versions of FILES by appending "~~". |
|
355 \end{ttbox} |
|
356 *} |
|
357 |
|
358 |
|
359 section {* Running Isabelle sessions \label{sec:tool-usedir} *} |
|
360 |
|
361 text {* The old @{tool_def usedir} tool builds object-logic images, or |
|
362 runs example sessions based on existing logics. Its usage is: |
|
363 \begin{ttbox} |
|
364 Usage: isabelle usedir [OPTIONS] LOGIC NAME |
|
365 |
|
366 Options are: |
|
367 -C BOOL copy existing document directory to -D PATH (default true) |
|
368 -D PATH dump generated document sources into PATH |
|
369 -M MAX multithreading: maximum number of worker threads (default 1) |
|
370 -P PATH set path for remote theory browsing information |
|
371 -Q INT set threshold for sub-proof parallelization (default 50) |
|
372 -T LEVEL multithreading: trace level (default 0) |
|
373 -V VARIANT declare alternative document VARIANT |
|
374 -b build mode (output heap image, using current dir) |
|
375 -d FORMAT build document as FORMAT (default false) |
|
376 -f NAME use ML file NAME (default ROOT.ML) |
|
377 -g BOOL generate session graph image for document (default false) |
|
378 -i BOOL generate theory browser information (default false) |
|
379 -m MODE add print mode for output |
|
380 -p LEVEL set level of detail for proof objects (default 0) |
|
381 -q LEVEL set level of parallel proof checking (default 1) |
|
382 -r reset session path |
|
383 -s NAME override session NAME |
|
384 -t BOOL internal session timing (default false) |
|
385 -v BOOL be verbose (default false) |
|
386 |
|
387 Build object-logic or run examples. Also creates browsing |
|
388 information (HTML etc.) according to settings. |
|
389 |
|
390 ISABELLE_USEDIR_OPTIONS=... |
|
391 |
|
392 ML_PLATFORM=... |
|
393 ML_HOME=... |
|
394 ML_SYSTEM=... |
|
395 ML_OPTIONS=... |
|
396 \end{ttbox} |
|
397 |
|
398 Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS} |
|
399 setting is implicitly prefixed to \emph{any} @{tool usedir} |
|
400 call. Since the @{verbatim IsaMakefile}s of all object-logics |
|
401 distributed with Isabelle just invoke @{tool usedir} for the real |
|
402 work, one may control compilation options globally via above |
|
403 variable. In particular, generation of \rmindex{HTML} browsing |
|
404 information and document preparation is controlled here. |
|
405 *} |
|
406 |
|
407 |
|
408 subsubsection {* Options *} |
|
409 |
|
410 text {* |
|
411 Basically, there are two different modes of operation: \emph{build |
|
412 mode} (enabled through the @{verbatim "-b"} option) and |
|
413 \emph{example mode} (default). |
|
414 |
|
415 Calling @{tool usedir} with @{verbatim "-b"} runs @{executable |
|
416 "isabelle-process"} with input image @{verbatim LOGIC} and output to |
|
417 @{verbatim NAME}, as provided on the command line. This will be a |
|
418 batch session, running @{verbatim ROOT.ML} from the current |
|
419 directory and then quitting. It is assumed that @{verbatim ROOT.ML} |
|
420 contains all ML commands required to build the logic. |
|
421 |
|
422 In example mode, @{tool usedir} runs a read-only session of |
|
423 @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from |
|
424 within directory @{verbatim NAME}. It assumes that this file |
|
425 contains appropriate ML commands to run the desired examples. |
|
426 |
|
427 \medskip The @{verbatim "-i"} option controls theory browser data |
|
428 generation. It may be explicitly turned on or off --- as usual, the |
|
429 last occurrence of @{verbatim "-i"} on the command line wins. |
|
430 |
|
431 The @{verbatim "-P"} option specifies a path (or actual URL) to be |
|
432 prefixed to any \emph{non-local} reference of existing theories. |
|
433 Thus user sessions may easily link to existing Isabelle libraries |
|
434 already present on the WWW. |
|
435 |
|
436 The @{verbatim "-m"} options specifies additional print modes to be |
|
437 activated temporarily while the session is processed. |
|
438 |
|
439 \medskip The @{verbatim "-d"} option controls document preparation. |
|
440 Valid arguments are @{verbatim false} (do not prepare any document; |
|
441 this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz}, |
|
442 @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}. The logic |
|
443 session has to provide a properly setup @{verbatim document} |
|
444 directory. See \secref{sec:tool-document} and |
|
445 \secref{sec:tool-latex} for more details. |
|
446 |
|
447 \medskip The @{verbatim "-V"} option declares alternative document |
|
448 variants, consisting of name/tags pairs (cf.\ options @{verbatim |
|
449 "-n"} and @{verbatim "-t"} of @{tool_ref document}). The standard |
|
450 document is equivalent to ``@{verbatim |
|
451 "document=theory,proof,ML"}'', which means that all theory begin/end |
|
452 commands, proof body texts, and ML code will be presented |
|
453 faithfully. |
|
454 |
|
455 An alternative variant ``@{verbatim "outline=/proof/ML"}'' would |
|
456 fold proof and ML parts, replacing the original text by a short |
|
457 place-holder. The form ``@{text name}@{verbatim "=-"},'' means to |
|
458 remove document @{text name} from the list of variants to be |
|
459 processed. Any number of @{verbatim "-V"} options may be given; |
|
460 later declarations have precedence over earlier ones. |
|
461 |
|
462 Some document variant @{text name} may use an alternative {\LaTeX} |
|
463 entry point called @{verbatim "document/root_"}@{text |
|
464 "name"}@{verbatim ".tex"} if that file exists; otherwise the common |
|
465 @{verbatim "document/root.tex"} is used. |
|
466 |
|
467 \medskip The @{verbatim "-g"} option produces images of the theory |
|
468 dependency graph (cf.\ \secref{sec:browse}) for inclusion in the |
|
469 generated document, both as @{verbatim session_graph.eps} and |
|
470 @{verbatim session_graph.pdf} at the same time. To include this in |
|
471 the final {\LaTeX} document one could say @{verbatim |
|
472 "\\includegraphics{session_graph}"} in @{verbatim |
|
473 "document/root.tex"} (omitting the file-name extension enables |
|
474 {\LaTeX} to select to correct version, either for the DVI or PDF |
|
475 output path). |
|
476 |
|
477 \medskip The @{verbatim "-D"} option causes the generated document |
|
478 sources to be dumped at location @{verbatim PATH}; this path is |
|
479 relative to the session's main directory. If the @{verbatim "-C"} |
|
480 option is true, this will include a copy of an existing @{verbatim |
|
481 document} directory as provided by the user. For example, @{tool |
|
482 usedir}~@{verbatim "-D generated HOL Foo"} produces a complete set |
|
483 of document sources at @{verbatim "Foo/generated"}. Subsequent |
|
484 invocation of @{tool document}~@{verbatim "Foo/generated"} (see also |
|
485 \secref{sec:tool-document}) will process the final result |
|
486 independently of an Isabelle job. This decoupled mode of operation |
|
487 facilitates debugging of serious {\LaTeX} errors, for example. |
|
488 |
|
489 \medskip The @{verbatim "-p"} option determines the level of detail |
|
490 for internal proof objects, see also the \emph{Isabelle Reference |
|
491 Manual}~\cite{isabelle-ref}. |
|
492 |
|
493 \medskip The @{verbatim "-q"} option specifies the level of parallel |
|
494 proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel |
|
495 proofs (default), @{verbatim 2} toplevel and nested Isar proofs. |
|
496 The option @{verbatim "-Q"} specifies a threshold for @{verbatim |
|
497 "-q2"}: nested proofs are only parallelized when the current number |
|
498 of forked proofs falls below the given value (default 50), |
|
499 multiplied by the number of worker threads (see option @{verbatim |
|
500 "-M"}). |
|
501 |
|
502 \medskip The @{verbatim "-t"} option produces a more detailed |
|
503 internal timing report of the session. |
|
504 |
|
505 \medskip The @{verbatim "-v"} option causes additional information |
|
506 to be printed while running the session, notably the location of |
|
507 prepared documents. |
|
508 |
|
509 \medskip The @{verbatim "-M"} option specifies the maximum number of |
|
510 parallel worker threads used for processing independent tasks when |
|
511 checking theory sources (multithreading only works on suitable ML |
|
512 platforms). The special value of @{verbatim 0} or @{verbatim max} |
|
513 refers to the number of actual CPU cores of the underlying machine, |
|
514 which is a good starting point for optimal performance tuning. The |
|
515 @{verbatim "-T"} option determines the level of detail in tracing |
|
516 output concerning the internal locking and scheduling in |
|
517 multithreaded operation. This may be helpful in isolating |
|
518 performance bottle-necks, e.g.\ due to excessive wait states when |
|
519 locking critical code sections. |
|
520 |
|
521 \medskip Any @{tool usedir} session is named by some \emph{session |
|
522 identifier}. These accumulate, documenting the way sessions depend |
|
523 on others. For example, consider @{verbatim "Pure/FOL/ex"}, which |
|
524 refers to the examples of FOL, which in turn is built upon Pure. |
|
525 |
|
526 The current session's identifier is by default just the base name of |
|
527 the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim |
|
528 NAME} argument (in example mode). This may be overridden explicitly |
|
529 via the @{verbatim "-s"} option. |
|
530 *} |
|
531 |
|
532 |
|
533 section {* Output the version identifier of the Isabelle distribution *} |
|
534 |
|
535 text {* |
|
536 The @{tool_def version} tool displays Isabelle version information: |
|
537 \begin{ttbox} |
|
538 Usage: isabelle version [OPTIONS] |
|
539 |
|
540 Options are: |
|
541 -i short identification (derived from Mercurial id) |
|
542 |
|
543 Display Isabelle version information. |
|
544 \end{ttbox} |
|
545 |
|
546 \medskip The default is to output the full version string of the |
|
547 Isabelle distribution, e.g.\ ``@{verbatim "Isabelle2012: May 2012"}. |
|
548 |
|
549 The @{verbatim "-i"} option produces a short identification derived |
|
550 from the Mercurial id of the @{setting ISABELLE_HOME} directory. |
|
551 *} |
|
552 |
|
553 |
|
554 section {* Convert XML to YXML *} |
|
555 |
|
556 text {* |
|
557 The @{tool_def yxml} tool converts a standard XML document (stdin) |
|
558 to the much simpler and more efficient YXML format of Isabelle |
|
559 (stdout). The YXML format is defined as follows. |
|
560 |
|
561 \begin{enumerate} |
|
562 |
|
563 \item The encoding is always UTF-8. |
|
564 |
|
565 \item Body text is represented verbatim (no escaping, no special |
|
566 treatment of white space, no named entities, no CDATA chunks, no |
|
567 comments). |
|
568 |
|
569 \item Markup elements are represented via ASCII control characters |
|
570 @{text "\<^bold>X = 5"} and @{text "\<^bold>Y = 6"} as follows: |
|
571 |
|
572 \begin{tabular}{ll} |
|
573 XML & YXML \\\hline |
|
574 @{verbatim "<"}@{text "name attribute"}@{verbatim "="}@{text "value \<dots>"}@{verbatim ">"} & |
|
575 @{text "\<^bold>X\<^bold>Yname\<^bold>Yattribute"}@{verbatim "="}@{text "value\<dots>\<^bold>X"} \\ |
|
576 @{verbatim "</"}@{text name}@{verbatim ">"} & @{text "\<^bold>X\<^bold>Y\<^bold>X"} \\ |
|
577 \end{tabular} |
|
578 |
|
579 There is no special case for empty body text, i.e.\ @{verbatim |
|
580 "<foo/>"} is treated like @{verbatim "<foo></foo>"}. Also note that |
|
581 @{text "\<^bold>X"} and @{text "\<^bold>Y"} may never occur in |
|
582 well-formed XML documents. |
|
583 |
|
584 \end{enumerate} |
|
585 |
|
586 Parsing YXML is pretty straight-forward: split the text into chunks |
|
587 separated by @{text "\<^bold>X"}, then split each chunk into |
|
588 sub-chunks separated by @{text "\<^bold>Y"}. Markup chunks start |
|
589 with an empty sub-chunk, and a second empty sub-chunk indicates |
|
590 close of an element. Any other non-empty chunk consists of plain |
|
591 text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or |
|
592 @{file "~~/src/Pure/PIDE/yxml.scala"}. |
|
593 |
|
594 YXML documents may be detected quickly by checking that the first |
|
595 two characters are @{text "\<^bold>X\<^bold>Y"}. |
|
596 *} |
|
597 |
|
598 end |
|