author | wenzelm |
Fri, 16 Feb 2007 22:13:16 +0100 | |
changeset 22332 | 3ddd31fa45fd |
parent 22155 | 47b36483f872 |
child 22376 | b711c2ad7507 |
permissions | -rw-r--r-- |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Thy/ml_context.ML |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
4 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
5 |
ML context and antiquotations. |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
6 |
*) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
7 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
8 |
signature BASIC_ML_CONTEXT = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
9 |
sig |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
10 |
val the_context: unit -> theory |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
11 |
val thm: xstring -> thm |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
12 |
val thms: xstring -> thm list |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
13 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
14 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
15 |
signature ML_CONTEXT = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
16 |
sig |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
17 |
include BASIC_ML_CONTEXT |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
18 |
val get_context: unit -> Context.generic option |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
19 |
val set_context: Context.generic option -> unit |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
20 |
val setmp: Context.generic option -> ('a -> 'b) -> 'a -> 'b |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
21 |
val the_generic_context: unit -> Context.generic |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
22 |
val the_local_context: unit -> Proof.context |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
23 |
val pass: Context.generic option -> ('a -> 'b) -> 'a -> 'b * Context.generic option |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
24 |
val pass_context: Context.generic -> ('a -> 'b) -> 'a -> 'b * Context.generic |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
25 |
val save: ('a -> 'b) -> 'a -> 'b |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
26 |
val >> : (theory -> theory) -> unit |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
27 |
val add_keywords: string list -> unit |
22136 | 28 |
val inline_antiq: string -> |
29 |
(Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit |
|
30 |
val value_antiq: string -> |
|
31 |
(Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
32 |
val use_mltext: string -> bool -> Context.generic option -> unit |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
33 |
val use_mltext_update: string -> bool -> Context.generic -> Context.generic |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
34 |
val use_let: string -> string -> string -> Context.generic -> Context.generic |
22146 | 35 |
val use: Path.T -> unit |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
36 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
37 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
38 |
structure ML_Context: ML_CONTEXT = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
39 |
struct |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
40 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
41 |
(** Implicit ML context **) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
42 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
43 |
local |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
44 |
val current_context = ref (NONE: Context.generic option); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
45 |
in |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
46 |
fun get_context () = ! current_context; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
47 |
fun set_context opt_context = current_context := opt_context; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
48 |
fun setmp opt_context f x = Library.setmp current_context opt_context f x; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
49 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
50 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
51 |
fun the_generic_context () = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
52 |
(case get_context () of |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
53 |
SOME context => context |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
54 |
| _ => error "Unknown context"); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
55 |
|
22136 | 56 |
val the_local_context = Context.proof_of o the_generic_context; |
57 |
||
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
58 |
val the_context = Context.theory_of o the_generic_context; |
22136 | 59 |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
60 |
fun pass opt_context f x = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
61 |
setmp opt_context (fn x => let val y = f x in (y, get_context ()) end) x; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
62 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
63 |
fun pass_context context f x = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
64 |
(case pass (SOME context) f x of |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
65 |
(y, SOME context') => (y, context') |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
66 |
| (_, NONE) => error "Lost context in ML"); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
67 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
68 |
fun save f x = setmp (get_context ()) f x; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
69 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
70 |
fun change_theory f = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
71 |
set_context (SOME (Context.map_theory f (the_generic_context ()))); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
72 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
73 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
74 |
(** ML antiquotations **) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
75 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
76 |
(* maintain keywords *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
77 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
78 |
val global_lexicon = ref Scan.empty_lexicon; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
79 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
80 |
fun add_keywords keywords = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
81 |
change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords)); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
82 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
83 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
84 |
(* maintain commands *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
85 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
86 |
datatype antiq = Inline of string | Value of string * string; |
22136 | 87 |
val global_parsers = ref (Symtab.empty: |
88 |
(Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table); |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
89 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
90 |
local |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
91 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
92 |
fun add_item kind name scan = change global_parsers (fn tab => |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
93 |
(if not (Symtab.defined tab name) then () |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
94 |
else warning ("Redefined ML antiquotation: " ^ quote name); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
95 |
Symtab.update (name, scan >> kind) tab)); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
96 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
97 |
in |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
98 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
99 |
val inline_antiq = add_item Inline; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
100 |
val value_antiq = add_item Value; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
101 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
102 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
103 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
104 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
105 |
(* command syntax *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
106 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
107 |
fun syntax scan src = |
22136 | 108 |
#1 (Args.context_syntax "ML antiquotation" scan src (the_local_context ())); |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
109 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
110 |
fun command src = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
111 |
let val ((name, _), pos) = Args.dest_src src in |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
112 |
(case Symtab.lookup (! global_parsers) name of |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
113 |
NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
114 |
| SOME scan => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
115 |
(fn () => syntax scan src) ()) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
116 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
117 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
118 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
119 |
(* outer syntax *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
120 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
121 |
structure T = OuterLex; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
122 |
structure P = OuterParse; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
123 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
124 |
val antiq = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
125 |
P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
126 |
>> (fn ((x, pos), y) => Args.src ((x, y), pos)); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
127 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
128 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
129 |
(* input/output wrappers *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
130 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
131 |
local |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
132 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
133 |
val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;"; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
134 |
val isabelle_struct0 = isabelle_struct ""; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
135 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
136 |
fun eval_antiquotes txt = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
137 |
let |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
138 |
val ants = Antiquote.scan_antiquotes (txt, Position.line 1); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
139 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
140 |
fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
141 |
| expand (Antiquote.Antiq x) names = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
142 |
(case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of |
22155 | 143 |
Inline s => (("", ML_Syntax.atomic s), names) |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
144 |
| Value (a, s) => |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
145 |
let |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
146 |
val a' = if ML_Syntax.is_identifier a then a else "val"; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
147 |
val ([b], names') = Name.variants [a'] names; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
148 |
in (("val " ^ b ^ " = " ^ s ^ ";\n", "Isabelle." ^ b), names') end); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
149 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
150 |
val (decls, body) = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
151 |
fold_map expand ants ML_Syntax.reserved |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
152 |
|> #1 |> split_list |> pairself implode; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
153 |
in (isabelle_struct decls, body) end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
154 |
|
22146 | 155 |
fun eval name verbose txt = |
156 |
Output.ML_errors (use_text name Output.ml_output verbose) txt; |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
157 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
158 |
in |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
159 |
|
22146 | 160 |
fun eval_wrapper name verbose txt = |
22136 | 161 |
let |
162 |
val (txt1, txt2) = eval_antiquotes txt; |
|
22332 | 163 |
val _ = |
164 |
if txt1 = isabelle_struct0 andalso txt2 = txt then () |
|
165 |
else Output.debug (fn () => cat_lines [txt1, txt2]); |
|
22146 | 166 |
in eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0 end; |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
167 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
168 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
169 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
170 |
|
22136 | 171 |
(* ML evaluation *) |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
172 |
|
22146 | 173 |
fun use_mltext txt verbose opt_context = |
174 |
setmp opt_context (fn () => eval_wrapper "ML" verbose txt) (); |
|
175 |
||
176 |
fun use_mltext_update txt verbose context = |
|
177 |
#2 (pass_context context (eval_wrapper "ML" verbose) txt); |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
178 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
179 |
fun use_context txt = use_mltext_update |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
180 |
("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
181 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
182 |
fun use_let bind body txt = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
183 |
use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
184 |
|
22146 | 185 |
fun use path = eval_wrapper (Path.implode path) true (File.read path); |
186 |
||
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
187 |
|
22136 | 188 |
(* basic antiquotations *) |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
189 |
|
22155 | 190 |
val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()")); |
191 |
||
22136 | 192 |
val _ = inline_antiq "typ" (Args.typ >> ML_Syntax.print_typ); |
193 |
val _ = inline_antiq "term" (Args.term >> ML_Syntax.print_term); |
|
194 |
val _ = inline_antiq "prop" (Args.prop >> ML_Syntax.print_term); |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
195 |
|
22136 | 196 |
val _ = value_antiq "ctyp" (Args.typ >> (fn T => |
22155 | 197 |
("ctyp", |
198 |
"Thm.ctyp_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)))); |
|
22136 | 199 |
|
200 |
val _ = value_antiq "cterm" (Args.term >> (fn t => |
|
22155 | 201 |
("cterm", |
202 |
"Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
|
22136 | 203 |
|
204 |
val _ = value_antiq "cprop" (Args.prop >> (fn t => |
|
22155 | 205 |
("cprop", |
206 |
"Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
|
207 |
||
208 |
||
209 |
||
210 |
(** fact references **) |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
211 |
|
22155 | 212 |
fun thm name = ProofContext.get_thm (the_local_context ()) (Name name); |
213 |
fun thms name = ProofContext.get_thms (the_local_context ()) (Name name); |
|
214 |
||
215 |
||
216 |
local |
|
217 |
||
218 |
fun print_interval (FromTo arg) = |
|
219 |
"PureThy.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg |
|
220 |
| print_interval (From i) = "PureThy.From " ^ ML_Syntax.print_int i |
|
221 |
| print_interval (Single i) = "PureThy.Single " ^ ML_Syntax.print_int i; |
|
22136 | 222 |
|
22155 | 223 |
fun thm_sel name = |
224 |
Args.thm_sel >> (fn is => "PureThy.NameSelection " ^ |
|
225 |
ML_Syntax.print_pair ML_Syntax.print_string (ML_Syntax.print_list print_interval) (name, is)) |
|
226 |
|| Scan.succeed ("PureThy.Name " ^ ML_Syntax.print_string name); |
|
227 |
||
228 |
fun thm_antiq kind = value_antiq kind |
|
229 |
(Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel => |
|
230 |
"ProofContext.get_" ^ kind ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel)); |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
231 |
|
22155 | 232 |
in |
233 |
||
234 |
val _ = add_keywords ["(", ")", "-", ","]; |
|
235 |
val _ = thm_antiq "thm"; |
|
236 |
val _ = thm_antiq "thms"; |
|
237 |
||
238 |
end; |
|
239 |
||
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
240 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
241 |
(*final declarations of this structure!*) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
242 |
nonfix >>; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
243 |
fun >> f = change_theory f; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
244 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
245 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
246 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
247 |
structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
248 |
open Basic_ML_Context; |