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 {*
|
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
|
260
|
14 |
fun propagate_env (context as Context.Proof lthy) =
|
|
15 |
Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
|
264
|
16 |
| propagate_env context = context
|
210
|
17 |
|
260
|
18 |
fun propagate_env_prf prf = Proof.map_contexts
|
264
|
19 |
(Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf
|
210
|
20 |
|
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
|
21 |
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
|
22 |
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
|
23 |
(OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
|
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
|
24 |
(OuterParse.ML_source >> (fn (txt, pos) =>
|
210
|
25 |
Toplevel.generic_theory
|
264
|
26 |
(ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)))
|
210
|
27 |
|
|
28 |
val _ =
|
|
29 |
OuterSyntax.command "ML_prf" "ML text within proof"
|
|
30 |
(OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl)
|
|
31 |
(OuterParse.ML_source >> (fn (txt, pos) =>
|
|
32 |
Toplevel.proof (Proof.map_context (Context.proof_map
|
260
|
33 |
(ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)))
|
210
|
34 |
|
224
|
35 |
val _ =
|
|
36 |
OuterSyntax.command "ML_val" "diagnostic ML text"
|
|
37 |
(OuterKeyword.tag "TutorialML" OuterKeyword.diag)
|
264
|
38 |
(OuterParse.ML_source >> IsarCmd.ml_diag true)
|
224
|
39 |
|
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
|
40 |
*}
|
239
|
41 |
|
|
42 |
end |