| author | Christian Urban <urbanc@in.tum.de> |
| Wed, 22 Jul 2009 01:10:14 +0200 | |
| changeset 278 | c6b64fa9f301 |
| parent 264 | 311830b43f8f |
| child 301 | 2728e8daebc0 |
| permissions | -rw-r--r-- |
| 23 | 1 |
theory Base |
| 264 | 2 |
imports Main LaTeXsugar |
| 23 | 3 |
uses |
|
256
1fb8d62c88a0
added some first index-information
Christian Urban <urbanc@in.tum.de>
parents:
255
diff
changeset
|
4 |
"output_tutorial.ML" |
|
57
065f472c09ab
Repaired output of marginal comments in ML antiquotation.
berghofe
parents:
43
diff
changeset
|
5 |
"chunks.ML" |
| 23 | 6 |
"antiquote_setup.ML" |
7 |
begin |
|
8 |
||
|
64
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
9 |
(* to have a special tag for text enclosed in ML *) |
|
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
10 |
ML {*
|
|
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
11 |
|
|
260
5accec94b6df
updated to lates Isabelle changes
Christian Urban <urbanc@in.tum.de>
parents:
256
diff
changeset
|
12 |
fun propagate_env (context as Context.Proof lthy) = |
|
5accec94b6df
updated to lates Isabelle changes
Christian Urban <urbanc@in.tum.de>
parents:
256
diff
changeset
|
13 |
Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy) |
| 264 | 14 |
| propagate_env context = context |
|
210
db8e302f44c8
more work on the simple inductive section
Christian Urban <urbanc@in.tum.de>
parents:
189
diff
changeset
|
15 |
|
|
260
5accec94b6df
updated to lates Isabelle changes
Christian Urban <urbanc@in.tum.de>
parents:
256
diff
changeset
|
16 |
fun propagate_env_prf prf = Proof.map_contexts |
| 264 | 17 |
(Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf |
|
210
db8e302f44c8
more work on the simple inductive section
Christian Urban <urbanc@in.tum.de>
parents:
189
diff
changeset
|
18 |
|
|
64
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
19 |
val _ = |
|
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
20 |
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>
parents:
80
diff
changeset
|
21 |
(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>
parents:
57
diff
changeset
|
22 |
(OuterParse.ML_source >> (fn (txt, pos) => |
|
210
db8e302f44c8
more work on the simple inductive section
Christian Urban <urbanc@in.tum.de>
parents:
189
diff
changeset
|
23 |
Toplevel.generic_theory |
| 264 | 24 |
(ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env))) |
|
210
db8e302f44c8
more work on the simple inductive section
Christian Urban <urbanc@in.tum.de>
parents:
189
diff
changeset
|
25 |
|
|
db8e302f44c8
more work on the simple inductive section
Christian Urban <urbanc@in.tum.de>
parents:
189
diff
changeset
|
26 |
val _ = |
|
db8e302f44c8
more work on the simple inductive section
Christian Urban <urbanc@in.tum.de>
parents:
189
diff
changeset
|
27 |
OuterSyntax.command "ML_prf" "ML text within proof" |
|
db8e302f44c8
more work on the simple inductive section
Christian Urban <urbanc@in.tum.de>
parents:
189
diff
changeset
|
28 |
(OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl) |
|
db8e302f44c8
more work on the simple inductive section
Christian Urban <urbanc@in.tum.de>
parents:
189
diff
changeset
|
29 |
(OuterParse.ML_source >> (fn (txt, pos) => |
|
db8e302f44c8
more work on the simple inductive section
Christian Urban <urbanc@in.tum.de>
parents:
189
diff
changeset
|
30 |
Toplevel.proof (Proof.map_context (Context.proof_map |
|
260
5accec94b6df
updated to lates Isabelle changes
Christian Urban <urbanc@in.tum.de>
parents:
256
diff
changeset
|
31 |
(ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf))) |
|
210
db8e302f44c8
more work on the simple inductive section
Christian Urban <urbanc@in.tum.de>
parents:
189
diff
changeset
|
32 |
|
|
224
647cab4a72c2
finished the heavy duty stuff for the inductive package
Christian Urban <urbanc@in.tum.de>
parents:
210
diff
changeset
|
33 |
val _ = |
|
647cab4a72c2
finished the heavy duty stuff for the inductive package
Christian Urban <urbanc@in.tum.de>
parents:
210
diff
changeset
|
34 |
OuterSyntax.command "ML_val" "diagnostic ML text" |
|
647cab4a72c2
finished the heavy duty stuff for the inductive package
Christian Urban <urbanc@in.tum.de>
parents:
210
diff
changeset
|
35 |
(OuterKeyword.tag "TutorialML" OuterKeyword.diag) |
| 264 | 36 |
(OuterParse.ML_source >> IsarCmd.ml_diag true) |
|
224
647cab4a72c2
finished the heavy duty stuff for the inductive package
Christian Urban <urbanc@in.tum.de>
parents:
210
diff
changeset
|
37 |
|
|
64
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
38 |
*} |
|
239
b63c72776f03
replaced "warning" with "writeln"
Christian Urban <urbanc@in.tum.de>
parents:
224
diff
changeset
|
39 |
|
|
255
ef1da1abee46
added infrastructure for index; antiquotations have now the options [index] and [indexc]
Christian Urban <urbanc@in.tum.de>
parents:
239
diff
changeset
|
40 |
|
|
239
b63c72776f03
replaced "warning" with "writeln"
Christian Urban <urbanc@in.tum.de>
parents:
224
diff
changeset
|
41 |
end |