1 |
1 |
2 theory Antiquotes |
2 theory Antiquotes |
3 imports Main |
3 imports "../Base" |
4 begin |
4 begin |
5 |
5 |
6 |
6 |
7 section {* Two Document Antiquotations *} |
7 section {* Useful Document Antiquotations *} |
8 |
8 |
9 text {* |
9 text {* |
|
10 {\bf Problem:} |
|
11 How to keep ML-code included in a document in sync with the actual code.\smallskip |
10 |
12 |
11 For writing documents using Isabelle it is often uesful to use |
13 {\bf Solution:} This can be achieved using document antiquotations.\smallskip |
12 document antiquotations. Below we give the code for such an |
|
13 antiquotation that typesets ML-code and also checks whether |
|
14 the code is actually correct. In this way one can achieve that the |
|
15 document is always in sync with code. |
|
16 |
14 |
17 Below we introduce the antiquotation @{text "@{ML_checked \"\<dots>\"}"} which |
15 Document antiquotations are a convenient method for type-setting consitently |
18 takes a piece of code as argument. We will check this code by sending |
16 a group of items in a document. They can also be used for sophisticated |
19 the ML-expression @{text "val _ = \<dots>"} to the ML-compiler (i.e.~the |
17 \LaTeX hacking. |
20 function @{ML "ML_Context.eval_in"}). The code for this antiquotation |
18 |
21 is as follows: |
19 Below we give the code for two such |
|
20 antiquotations that can be used to typeset ML-code and also to check whether |
|
21 the code is actually compiles. In this way one can relatively easily |
|
22 keep documents in sync with code. |
|
23 |
|
24 We first describe the antiquotation @{text "@{ML_checked \"\<dots>\"}"} which |
|
25 takes a piece of code as argument. This code is checked by sending |
|
26 the ML-expression @{text "val _ = \<dots>"} containing the given code to the |
|
27 ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"}). The code |
|
28 for this antiquotation is as follows: |
22 *} |
29 *} |
23 |
30 |
24 ML {* |
31 ML {* |
25 fun ml_val txt = "val _ = " ^ txt |
32 fun ml_val txt = "val _ = " ^ txt |
26 |
33 |
27 fun output_ml ml src ctxt txt = |
34 fun output_ml ml src ctxt txt = |
28 (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt); |
35 (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt); |
29 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt)) |
36 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
|
37 (space_explode "\n" txt)) |
30 |
38 |
31 val _ = ThyOutput.add_commands |
39 val _ = ThyOutput.add_commands |
32 [("ML_checked", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val))] |
40 [("ML_checked", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val))] |
33 *} |
41 *} |
34 |
42 |
35 text {* |
43 text {* |
36 |
44 |
37 Note that the parser @{ML "(Scan.lift Args.name)"} parses a string. If the |
45 Note that the parser @{ML "(Scan.lift Args.name)"} parses a string. If the |
38 code is approved by the compiler, the output function |
46 code is approved by the compiler, the output function |
39 @{ML "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} |
47 @{ML "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} |
40 pretty prints the code. There are a number of options that are observed |
48 pretty prints the code. This function expects that the code is a list of strings |
41 when printing the code (for example @{text "[display]"}; for more information |
49 according to the line breaks (therefore the |
42 about the options see \rsccite{sec:antiq}). |
50 @{ML_open "(space_explode \"\\n\" txt)" for txt} which produces this list). |
|
51 There are a number of options that are observed by @{ML ThyOutput.output_list} |
|
52 when printing the code (for example @{text "[display]"} and @{text "[source]"}; |
|
53 for more information about these options see \rsccite{sec:antiq}). |
43 |
54 |
44 Since we |
55 Since we used the argument @{ML "Position.none"}, the compiler cannot give specific |
45 used the argument @{ML "Position.none"}, the compiler cannot give specific |
|
46 information about the line number where an error might have occurred. We |
56 information about the line number where an error might have occurred. We |
47 can improve this code slightly by writing |
57 can improve this code slightly by writing |
48 |
58 |
|
59 The second |
49 *} |
60 *} |
50 |
61 |
51 ML {* |
62 ML {* |
52 fun output_ml ml src ctxt (txt,pos) = |
63 fun output_ml ml src ctxt (txt,pos) = |
53 (ML_Context.eval_in (SOME ctxt) false pos (ml txt); |
64 (ML_Context.eval_in (SOME ctxt) false pos (ml txt); |
54 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt)) |
65 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
|
66 (space_explode "\n" txt)) |
55 |
67 |
56 val _ = ThyOutput.add_commands |
68 val _ = ThyOutput.add_commands |
57 [("ML_checked", ThyOutput.args |
69 [("ML_checked", ThyOutput.args |
58 (Scan.lift (OuterParse.position Args.name)) (output_ml ml_val))] |
70 (Scan.lift (OuterParse.position Args.name)) (output_ml ml_val))] |
59 *} |
71 *} |
60 |
72 |
61 text {* |
73 text {* |
62 where the antiquotation can also handle position information. |
|
63 |
|
64 (FIXME: say something about OuterParse.position) |
74 (FIXME: say something about OuterParse.position) |
65 |
|
66 *} |
75 *} |
67 |
76 |
68 ML {* |
77 ML {* |
69 |
|
70 fun ml_pat (rhs, pat) = |
78 fun ml_pat (rhs, pat) = |
71 let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat)) |
79 let val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
72 in |
80 in |
73 "val " ^ pat' ^ " = " ^ rhs |
81 "val " ^ pat' ^ " = " ^ rhs |
74 end; |
82 end; |
75 |
83 |
76 fun add_response_indicator txt = |
84 fun add_response_indicator txt = |