23
|
1 |
theory Base
|
264
|
2 |
imports Main LaTeXsugar
|
23
|
3 |
uses
|
256
|
4 |
"output_tutorial.ML"
|
57
|
5 |
"chunks.ML"
|
23
|
6 |
"antiquote_setup.ML"
|
|
7 |
begin
|
|
8 |
|
302
|
9 |
(* re-definition of various ML antiquotations *)
|
64
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
10 |
(* to have a special tag for text enclosed in ML *)
|
301
|
11 |
|
64
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
12 |
ML {*
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
(* FIXME ref *)
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
14 |
val file_name = ref (NONE : string option)
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
fun write_file txt =
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
case !file_name of
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
NONE => () (* error "No open file" *)
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
| SOME name =>
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
20 |
(let
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
val stream = TextIO.openAppend name
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
in
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
TextIO.output (stream, txt);
|
311
|
24 |
TextIO.flushOut stream; (* needed ?*)
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
TextIO.closeOut stream
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
end)
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
*}
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
29 |
ML {*
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
30 |
fun write_file_blk txt =
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
let
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
val pre = implode ["\n", "ML ", "{", "*", "\n"]
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
33 |
val post = implode ["\n", "*", "}", "\n"]
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
34 |
in
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
write_file (enclose pre post txt)
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
36 |
end
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
*}
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
ML {*
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
fun open_file name =
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
(tracing ("Opened File: " ^ name);
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
42 |
file_name := SOME name)
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
43 |
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
44 |
fun open_file_prelude name txt =
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
45 |
(open_file name; write_file (txt ^ "\n"))
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
*}
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
48 |
ML {*
|
64
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
|
260
|
50 |
fun propagate_env (context as Context.Proof lthy) =
|
|
51 |
Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
|
264
|
52 |
| propagate_env context = context
|
210
|
53 |
|
260
|
54 |
fun propagate_env_prf prf = Proof.map_contexts
|
264
|
55 |
(Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf
|
210
|
56 |
|
64
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
57 |
val _ =
|
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
58 |
OuterSyntax.command "ML" "eval ML text within theory"
|
106
bdd82350cf22
renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
59 |
(OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
60 |
(OuterParse.position OuterParse.text >> (fn (txt, pos) =>
|
210
|
61 |
Toplevel.generic_theory
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
62 |
(ML_Context.exec (fn () => (write_file_blk txt; ML_Context.eval true pos txt)) #> propagate_env)))
|
210
|
63 |
|
|
64 |
val _ =
|
|
65 |
OuterSyntax.command "ML_prf" "ML text within proof"
|
|
66 |
(OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl)
|
|
67 |
(OuterParse.ML_source >> (fn (txt, pos) =>
|
|
68 |
Toplevel.proof (Proof.map_context (Context.proof_map
|
260
|
69 |
(ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)))
|
210
|
70 |
|
224
|
71 |
val _ =
|
|
72 |
OuterSyntax.command "ML_val" "diagnostic ML text"
|
|
73 |
(OuterKeyword.tag "TutorialML" OuterKeyword.diag)
|
264
|
74 |
(OuterParse.ML_source >> IsarCmd.ml_diag true)
|
224
|
75 |
|
64
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
76 |
*}
|
239
|
77 |
|
|
78 |
end |