author | wenzelm |
Sun, 29 Jul 2007 16:00:05 +0200 | |
changeset 24056 | e134e757fc64 |
parent 23939 | e543359fe8b6 |
child 24149 | 1b2f1a1a03a3 |
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 |
|
22652 | 32 |
val proj_value_antiq: string -> (Context.generic * Args.T list -> |
33 |
(string * string * string) * (Context.generic * Args.T list)) -> unit |
|
22666 | 34 |
val eval_antiquotes_fn: (string -> string * string) ref (* FIXME tmp *) |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
35 |
val use_mltext: string -> bool -> Context.generic option -> unit |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
36 |
val use_mltext_update: string -> bool -> Context.generic -> Context.generic |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
37 |
val use_let: string -> string -> string -> Context.generic -> Context.generic |
22146 | 38 |
val use: Path.T -> unit |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
39 |
end; |
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 |
structure ML_Context: ML_CONTEXT = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
42 |
struct |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
43 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
44 |
(** Implicit ML context **) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
45 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
46 |
local |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
47 |
val current_context = ref (NONE: Context.generic option); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
48 |
in |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
49 |
fun get_context () = ! current_context; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
50 |
fun set_context opt_context = current_context := opt_context; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
51 |
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
|
52 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
53 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
54 |
fun the_generic_context () = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
55 |
(case get_context () of |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
56 |
SOME context => context |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
57 |
| _ => error "Unknown context"); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
58 |
|
22136 | 59 |
val the_local_context = Context.proof_of o the_generic_context; |
60 |
||
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
61 |
val the_context = Context.theory_of o the_generic_context; |
22136 | 62 |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
63 |
fun pass opt_context f x = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
64 |
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
|
65 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
66 |
fun pass_context context f x = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
67 |
(case pass (SOME context) f x of |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
68 |
(y, SOME context') => (y, context') |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
69 |
| (_, NONE) => error "Lost context in ML"); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
70 |
|
23939 | 71 |
fun save f x = CRITICAL (fn () => setmp (get_context ()) f x); |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
72 |
|
23939 | 73 |
fun change_theory f = CRITICAL (fn () => |
74 |
set_context (SOME (Context.map_theory f (the_generic_context ())))); |
|
75 |
||
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
76 |
|
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 |
(** ML antiquotations **) |
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 |
(* maintain keywords *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
81 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
82 |
val global_lexicon = ref Scan.empty_lexicon; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
83 |
|
23939 | 84 |
fun add_keywords keywords = CRITICAL (fn () => |
85 |
change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords))); |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
86 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
87 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
88 |
(* maintain commands *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
89 |
|
22652 | 90 |
datatype antiq = Inline of string | ProjValue of string * string * string; |
22136 | 91 |
val global_parsers = ref (Symtab.empty: |
92 |
(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
|
93 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
94 |
local |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
95 |
|
23939 | 96 |
fun add_item kind name scan = CRITICAL (fn () => |
97 |
change global_parsers (fn tab => |
|
98 |
(if not (Symtab.defined tab name) then () |
|
99 |
else warning ("Redefined ML antiquotation: " ^ quote name); |
|
100 |
Symtab.update (name, scan >> kind) tab))); |
|
22105
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 |
in |
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 |
val inline_antiq = add_item Inline; |
22652 | 105 |
val proj_value_antiq = add_item ProjValue; |
106 |
fun value_antiq name scan = proj_value_antiq name (scan >> (fn (a, s) => (a, s, ""))); |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
107 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
108 |
end; |
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 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
111 |
(* command syntax *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
112 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
113 |
fun syntax scan src = |
22136 | 114 |
#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
|
115 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
116 |
fun command src = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
117 |
let val ((name, _), pos) = Args.dest_src src in |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
118 |
(case Symtab.lookup (! global_parsers) name of |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
119 |
NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos) |
23939 | 120 |
| SOME scan => syntax scan src) |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
121 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
122 |
|
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 |
(* outer syntax *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
125 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
126 |
structure T = OuterLex; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
127 |
structure P = OuterParse; |
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 |
val antiq = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
130 |
P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
131 |
>> (fn ((x, pos), y) => Args.src ((x, y), pos)); |
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 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
134 |
(* input/output wrappers *) |
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 |
local |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
137 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
138 |
val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;"; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
139 |
val isabelle_struct0 = isabelle_struct ""; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
140 |
|
23939 | 141 |
fun eval_antiquotes txt = CRITICAL (fn () => |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
142 |
let |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
143 |
val ants = Antiquote.scan_antiquotes (txt, Position.line 1); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
144 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
145 |
fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
146 |
| expand (Antiquote.Antiq x) names = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
147 |
(case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of |
22621 | 148 |
Inline s => (("", s), names) |
22652 | 149 |
| ProjValue (a, s, f) => |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
150 |
let |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
151 |
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
|
152 |
val ([b], names') = Name.variants [a'] names; |
22663
73517244fc46
eval_antiquotes: proper parentheses for projection;
wenzelm
parents:
22652
diff
changeset
|
153 |
val binding = "val " ^ b ^ " = " ^ s ^ ";\n"; |
73517244fc46
eval_antiquotes: proper parentheses for projection;
wenzelm
parents:
22652
diff
changeset
|
154 |
val value = |
73517244fc46
eval_antiquotes: proper parentheses for projection;
wenzelm
parents:
22652
diff
changeset
|
155 |
if f = "" then "Isabelle." ^ b |
73517244fc46
eval_antiquotes: proper parentheses for projection;
wenzelm
parents:
22652
diff
changeset
|
156 |
else "(" ^ f ^ " Isabelle." ^ b ^ ")"; |
73517244fc46
eval_antiquotes: proper parentheses for projection;
wenzelm
parents:
22652
diff
changeset
|
157 |
in ((binding, value), names') end); |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
158 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
159 |
val (decls, body) = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
160 |
fold_map expand ants ML_Syntax.reserved |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
161 |
|> #1 |> split_list |> pairself implode; |
23939 | 162 |
in (isabelle_struct decls, body) end); |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
163 |
|
24056
e134e757fc64
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23939
diff
changeset
|
164 |
fun eval name verbose txt = use_text name Output.ml_output verbose txt; |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
165 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
166 |
in |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
167 |
|
22666 | 168 |
val eval_antiquotes_fn = ref eval_antiquotes; |
169 |
||
22146 | 170 |
fun eval_wrapper name verbose txt = |
22136 | 171 |
let |
22666 | 172 |
val (txt1, txt2) = ! eval_antiquotes_fn txt; |
22332 | 173 |
val _ = |
174 |
if txt1 = isabelle_struct0 andalso txt2 = txt then () |
|
175 |
else Output.debug (fn () => cat_lines [txt1, txt2]); |
|
22146 | 176 |
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
|
177 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
178 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
179 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
180 |
|
22136 | 181 |
(* ML evaluation *) |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
182 |
|
22146 | 183 |
fun use_mltext txt verbose opt_context = |
184 |
setmp opt_context (fn () => eval_wrapper "ML" verbose txt) (); |
|
185 |
||
186 |
fun use_mltext_update txt verbose context = |
|
187 |
#2 (pass_context context (eval_wrapper "ML" verbose) txt); |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
188 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
189 |
fun use_context txt = use_mltext_update |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
190 |
("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
|
191 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
192 |
fun use_let bind body txt = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
193 |
use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
194 |
|
22146 | 195 |
fun use path = eval_wrapper (Path.implode path) true (File.read path); |
196 |
||
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
197 |
|
22136 | 198 |
(* basic antiquotations *) |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
199 |
|
22155 | 200 |
val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()")); |
201 |
||
22621 | 202 |
val _ = inline_antiq "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)); |
203 |
val _ = inline_antiq "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
|
204 |
val _ = inline_antiq "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)); |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
205 |
|
22136 | 206 |
val _ = value_antiq "ctyp" (Args.typ >> (fn T => |
22155 | 207 |
("ctyp", |
208 |
"Thm.ctyp_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)))); |
|
22136 | 209 |
|
210 |
val _ = value_antiq "cterm" (Args.term >> (fn t => |
|
22155 | 211 |
("cterm", |
212 |
"Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
|
22136 | 213 |
|
214 |
val _ = value_antiq "cprop" (Args.prop >> (fn t => |
|
22155 | 215 |
("cprop", |
216 |
"Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)))); |
|
217 |
||
218 |
||
22376 | 219 |
fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) => |
220 |
#1 (Term.dest_Const (Consts.read_const (ProofContext.consts_of ctxt) c)) |
|
221 |
|> syn ? ProofContext.const_syntax_name ctxt |
|
222 |
|> ML_Syntax.print_string); |
|
223 |
||
224 |
val _ = inline_antiq "const_name" (const false); |
|
225 |
val _ = inline_antiq "const_syntax" (const true); |
|
226 |
||
227 |
||
22155 | 228 |
|
229 |
(** fact references **) |
|
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
230 |
|
22155 | 231 |
fun thm name = ProofContext.get_thm (the_local_context ()) (Name name); |
232 |
fun thms name = ProofContext.get_thms (the_local_context ()) (Name name); |
|
233 |
||
234 |
||
235 |
local |
|
236 |
||
237 |
fun print_interval (FromTo arg) = |
|
238 |
"PureThy.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg |
|
239 |
| print_interval (From i) = "PureThy.From " ^ ML_Syntax.print_int i |
|
240 |
| print_interval (Single i) = "PureThy.Single " ^ ML_Syntax.print_int i; |
|
22136 | 241 |
|
22155 | 242 |
fun thm_sel name = |
243 |
Args.thm_sel >> (fn is => "PureThy.NameSelection " ^ |
|
244 |
ML_Syntax.print_pair ML_Syntax.print_string (ML_Syntax.print_list print_interval) (name, is)) |
|
245 |
|| Scan.succeed ("PureThy.Name " ^ ML_Syntax.print_string name); |
|
246 |
||
247 |
fun thm_antiq kind = value_antiq kind |
|
248 |
(Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel => |
|
249 |
"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
|
250 |
|
22155 | 251 |
in |
252 |
||
253 |
val _ = add_keywords ["(", ")", "-", ","]; |
|
254 |
val _ = thm_antiq "thm"; |
|
255 |
val _ = thm_antiq "thms"; |
|
256 |
||
257 |
end; |
|
258 |
||
23033
a7e23f993c5e
added cpat antiquotation for reading certified patterns
chaieb
parents:
22666
diff
changeset
|
259 |
val _ = proj_value_antiq "cpat" (Scan.lift Args.name >> |
a7e23f993c5e
added cpat antiquotation for reading certified patterns
chaieb
parents:
22666
diff
changeset
|
260 |
(fn ns => ("cpat", |
a7e23f993c5e
added cpat antiquotation for reading certified patterns
chaieb
parents:
22666
diff
changeset
|
261 |
"((cterm_of (ML_Context.the_context ())) o Library.the_single o " ^ |
a7e23f993c5e
added cpat antiquotation for reading certified patterns
chaieb
parents:
22666
diff
changeset
|
262 |
"(ProofContext.read_term_pats TypeInfer.logicT (ML_Context.the_local_context ())))" |
a7e23f993c5e
added cpat antiquotation for reading certified patterns
chaieb
parents:
22666
diff
changeset
|
263 |
^ (ML_Syntax.print_list ML_Syntax.print_string [ns]), ""))); |
22105
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
264 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
265 |
(*final declarations of this structure!*) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
266 |
nonfix >>; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
267 |
fun >> f = change_theory f; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
268 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
269 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
270 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
271 |
structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
272 |
open Basic_ML_Context; |