1 theory Base |
1 theory Base |
2 imports Main LaTeXsugar |
2 imports Main LaTeXsugar |
3 uses |
3 uses |
4 "output_tutorial.ML" |
4 ("output_tutorial.ML") |
5 "antiquote_setup.ML" |
5 ("antiquote_setup.ML") |
6 begin |
6 begin |
7 |
7 |
8 (* rebinding of writeln and tracing so that it can *) |
8 (* rebinding of writeln and tracing so that it can *) |
9 (* be compared in intiquotations *) |
9 (* be compared in intiquotations *) |
10 ML {* |
10 ML {* |
11 fun writeln s = (Output.writeln s; s) |
11 fun writeln s = (Output.writeln s; s) |
12 fun tracing s = (Output.tracing s; s) |
12 fun tracing s = (Output.tracing s; s) |
13 *} |
13 *} |
14 |
14 |
15 (* re-definition of various ML antiquotations *) |
15 (* re-definition of various ML antiquotations *) |
16 (* to have a special tag for text enclosed in ML *) |
16 (* to have a special tag for text enclosed in ML; *) |
|
17 (* they also write the code into a separate file *) |
17 |
18 |
18 ML {* |
19 ML {* |
19 (* FIXME ref *) |
20 val (filename, setup_filename) = Attrib.config_string "filename" "File_Code.ML" |
20 val file_name = Unsynchronized.ref (NONE : string option) |
|
21 |
|
22 fun write_file txt = |
|
23 case !file_name of |
|
24 NONE => () (* error "No open file" *) |
|
25 | SOME name => |
|
26 (let |
|
27 val stream = TextIO.openAppend name |
|
28 in |
|
29 TextIO.output (stream, txt); |
|
30 TextIO.flushOut stream; (* needed ?*) |
|
31 TextIO.closeOut stream |
|
32 end) |
|
33 *} |
21 *} |
34 |
22 |
|
23 setup {* setup_filename *} |
|
24 |
35 ML {* |
25 ML {* |
36 fun write_file_blk txt = |
26 fun write_file txt thy = |
37 let |
27 let |
38 val pre = implode ["\n", "ML ", "{", "*", "\n"] |
28 val stream = Config.get_thy thy filename |
39 val post = implode ["\n", "*", "}", "\n"] |
29 |> TextIO.openAppend |
40 in |
30 in |
41 write_file (enclose pre post txt) |
31 TextIO.output (stream, txt); |
|
32 TextIO.flushOut stream; (* needed ?*) |
|
33 TextIO.closeOut stream |
42 end |
34 end |
43 *} |
35 *} |
44 |
36 |
45 ML {* |
37 ML {* |
46 fun open_file name = |
38 fun write_file_ml_blk txt thy = |
47 (tracing ("Opened File: " ^ name); |
39 let |
48 file_name := SOME name; |
40 val pre = implode ["\n", "ML ", "{", "*", "\n"] |
49 TextIO.openOut name; ()) |
41 val post = implode ["\n", "*", "}", "\n"] |
|
42 val _ = write_file (enclose pre post txt) thy |
|
43 in |
|
44 thy |
|
45 end |
50 |
46 |
51 fun open_file_prelude name txt = |
47 fun write_file_setup_blk txt thy = |
52 (open_file name; write_file (txt ^ "\n")) |
48 let |
|
49 val pre = implode ["\n", "setup ", "{", "*", "\n"] |
|
50 val post = implode ["\n", "*", "}", "\n"] |
|
51 val _ = write_file (enclose pre post txt) thy |
|
52 in |
|
53 thy |
|
54 end |
|
55 |
|
56 fun write_file_lsetup_blk txt lthy = |
|
57 let |
|
58 val pre = implode ["\n", "local_setup ", "{", "*", "\n"] |
|
59 val post = implode ["\n", "*", "}", "\n"] |
|
60 val _ = write_file (enclose pre post txt) (ProofContext.theory_of lthy) |
|
61 in |
|
62 lthy |
|
63 end |
|
64 |
53 *} |
65 *} |
54 |
66 |
55 ML {* |
67 ML {* |
|
68 fun open_file name thy = |
|
69 let |
|
70 val _ = tracing ("Open File: " ^ name) |
|
71 val _ = TextIO.openOut name |
|
72 in |
|
73 Config.put_thy filename name thy |
|
74 end |
|
75 *} |
56 |
76 |
|
77 ML {* |
|
78 fun open_file_with_prelude name txts thy = |
|
79 let |
|
80 val thy' = open_file name thy |
|
81 val _ = write_file (cat_lines txts) thy' |
|
82 in |
|
83 thy' |
|
84 end |
|
85 *} |
|
86 |
|
87 ML {* |
57 fun propagate_env (context as Context.Proof lthy) = |
88 fun propagate_env (context as Context.Proof lthy) = |
58 Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy) |
89 Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy) |
59 | propagate_env context = context |
90 | propagate_env context = context |
60 |
91 |
61 fun propagate_env_prf prf = Proof.map_contexts |
92 fun propagate_env_prf prf = Proof.map_contexts |
62 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
93 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
|
94 *} |
63 |
95 |
|
96 ML {* |
64 val _ = |
97 val _ = |
65 OuterSyntax.command "ML" "eval ML text within theory" |
98 OuterSyntax.command "ML" "eval ML text within theory" |
66 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
99 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
67 (OuterParse.position OuterParse.text >> (fn (txt, pos) => |
100 (OuterParse.position OuterParse.text >> |
68 Toplevel.generic_theory |
101 (fn (txt, pos) => |
69 (ML_Context.exec (fn () => (write_file_blk txt; ML_Context.eval true pos txt)) #> propagate_env))) |
102 Toplevel.generic_theory |
|
103 (ML_Context.exec |
|
104 (fn () => ML_Context.eval true pos txt) |
|
105 #> propagate_env #> Context.map_theory (write_file_ml_blk txt)))) |
70 |
106 |
71 val _ = |
107 val _ = |
72 OuterSyntax.command "ML_prf" "ML text within proof" |
108 OuterSyntax.command "ML_prf" "ML text within proof" |
73 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
109 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
74 (OuterParse.ML_source >> (fn (txt, pos) => |
110 (OuterParse.ML_source >> (fn (txt, pos) => |
77 |
113 |
78 val _ = |
114 val _ = |
79 OuterSyntax.command "ML_val" "diagnostic ML text" |
115 OuterSyntax.command "ML_val" "diagnostic ML text" |
80 (OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
116 (OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
81 (OuterParse.ML_source >> IsarCmd.ml_diag true) |
117 (OuterParse.ML_source >> IsarCmd.ml_diag true) |
82 |
|
83 *} |
118 *} |
84 |
119 |
|
120 ML {* |
|
121 val _ = |
|
122 OuterSyntax.command "setup" "ML theory setup" |
|
123 (OuterKeyword.tag_ml OuterKeyword.thy_decl) |
|
124 (OuterParse.ML_source >> (fn (txt, pos) => |
|
125 (Toplevel.theory (IsarCmd.global_setup (txt, pos) #> write_file_setup_blk txt)))) |
|
126 *} |
|
127 |
|
128 ML {* Context.proof_map *} |
|
129 ML {* IsarCmd.local_setup ; Context.map_proof (write_file_lsetup_blk "") *} |
|
130 |
|
131 |
|
132 ML {* |
|
133 val _ = |
|
134 OuterSyntax.local_theory "local_setup" "ML local theory setup" |
|
135 (OuterKeyword.tag_ml OuterKeyword.thy_decl) |
|
136 (OuterParse.ML_source >> (fn (txt, pos) => |
|
137 IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt)); |
|
138 *} |
|
139 |
|
140 |
|
141 use "output_tutorial.ML" |
|
142 use "antiquote_setup.ML" |
|
143 |
|
144 |
85 end |
145 end |