8 |
8 |
9 (* re-definition of various ML antiquotations *) |
9 (* re-definition of various ML antiquotations *) |
10 (* to have a special tag for text enclosed in ML *) |
10 (* to have a special tag for text enclosed in ML *) |
11 |
11 |
12 ML {* |
12 ML {* |
|
13 (* FIXME ref *) |
|
14 val file_name = ref (NONE : string option) |
|
15 |
|
16 fun write_file txt = |
|
17 case !file_name of |
|
18 NONE => () (* error "No open file" *) |
|
19 | SOME name => |
|
20 (let |
|
21 val stream = TextIO.openAppend name |
|
22 in |
|
23 TextIO.output (stream, txt); |
|
24 TextIO.flushOut stream; |
|
25 TextIO.closeOut stream |
|
26 end) |
|
27 *} |
|
28 |
|
29 ML {* |
|
30 fun write_file_blk txt = |
|
31 let |
|
32 val pre = implode ["\n", "ML ", "{", "*", "\n"] |
|
33 val post = implode ["\n", "*", "}", "\n"] |
|
34 in |
|
35 write_file (enclose pre post txt) |
|
36 end |
|
37 *} |
|
38 |
|
39 ML {* |
|
40 fun open_file name = |
|
41 (tracing ("Opened File: " ^ name); |
|
42 file_name := SOME name) |
|
43 |
|
44 fun open_file_prelude name txt = |
|
45 (open_file name; write_file (txt ^ "\n")) |
|
46 *} |
|
47 |
|
48 |
|
49 ML {* |
13 |
50 |
14 fun propagate_env (context as Context.Proof lthy) = |
51 fun propagate_env (context as Context.Proof lthy) = |
15 Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy) |
52 Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy) |
16 | propagate_env context = context |
53 | propagate_env context = context |
17 |
54 |
18 fun propagate_env_prf prf = Proof.map_contexts |
55 fun propagate_env_prf prf = Proof.map_contexts |
19 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
56 (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
|
57 *} |
20 |
58 |
|
59 ML {* |
21 val _ = |
60 val _ = |
22 OuterSyntax.command "ML" "eval ML text within theory" |
61 OuterSyntax.command "ML" "eval ML text within theory" |
23 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
62 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
24 (OuterParse.ML_source >> (fn (txt, pos) => |
63 (OuterParse.position OuterParse.text >> (fn (txt, pos) => |
25 Toplevel.generic_theory |
64 Toplevel.generic_theory |
26 (ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env))) |
65 (ML_Context.exec (fn () => (write_file_blk txt; ML_Context.eval true pos txt)) #> propagate_env))) |
|
66 *} |
27 |
67 |
|
68 ML {* |
28 val _ = |
69 val _ = |
29 OuterSyntax.command "ML_prf" "ML text within proof" |
70 OuterSyntax.command "ML_prf" "ML text within proof" |
30 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
71 (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
31 (OuterParse.ML_source >> (fn (txt, pos) => |
72 (OuterParse.ML_source >> (fn (txt, pos) => |
32 Toplevel.proof (Proof.map_context (Context.proof_map |
73 Toplevel.proof (Proof.map_context (Context.proof_map |
33 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))) |
74 (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))) |
|
75 *} |
34 |
76 |
|
77 ML {* |
35 val _ = |
78 val _ = |
36 OuterSyntax.command "ML_val" "diagnostic ML text" |
79 OuterSyntax.command "ML_val" "diagnostic ML text" |
37 (OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
80 (OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
38 (OuterParse.ML_source >> IsarCmd.ml_diag true) |
81 (OuterParse.ML_source >> IsarCmd.ml_diag true) |
39 |
82 |