author | wenzelm |
Fri, 19 Jan 2007 22:08:13 +0100 | |
changeset 22105 | ecdbab20c92c |
child 22136 | faff42afeacd |
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 |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
28 |
val inline_antiq: string -> (Args.T list -> string * Args.T list) -> unit |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
29 |
val value_antiq: string -> (Args.T list -> (string * string) * Args.T list) -> unit |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
30 |
val use_mltext: string -> bool -> Context.generic option -> unit |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
31 |
val use_mltext_update: string -> bool -> Context.generic -> Context.generic |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
32 |
val use_let: string -> string -> string -> Context.generic -> Context.generic |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
33 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
34 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
35 |
structure ML_Context: ML_CONTEXT = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
36 |
struct |
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 |
(** Implicit ML context **) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
39 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
40 |
local |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
41 |
val current_context = ref (NONE: Context.generic option); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
42 |
in |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
43 |
fun get_context () = ! current_context; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
44 |
fun set_context opt_context = current_context := opt_context; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
45 |
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
|
46 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
47 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
48 |
fun the_generic_context () = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
49 |
(case get_context () of |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
50 |
SOME context => context |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
51 |
| _ => error "Unknown context"); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
52 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
53 |
val the_context = Context.theory_of o the_generic_context; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
54 |
val the_local_context = Context.proof_of o the_generic_context; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
55 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
56 |
fun pass opt_context f x = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
57 |
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
|
58 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
59 |
fun pass_context context f x = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
60 |
(case pass (SOME context) f x of |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
61 |
(y, SOME context') => (y, context') |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
62 |
| (_, NONE) => error "Lost context in ML"); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
63 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
64 |
fun save f x = setmp (get_context ()) f 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 change_theory f = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
67 |
set_context (SOME (Context.map_theory f (the_generic_context ()))); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
68 |
|
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 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
71 |
(** ML antiquotations **) |
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 |
(* maintain keywords *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
74 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
75 |
val global_lexicon = ref Scan.empty_lexicon; |
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 |
fun add_keywords keywords = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
78 |
change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords)); |
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 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
81 |
(* maintain commands *) |
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 |
datatype antiq = Inline of string | Value of string * string; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
84 |
val global_parsers = ref (Symtab.empty: (Args.T list -> antiq * Args.T list) Symtab.table); |
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 |
local |
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 |
fun add_item kind name scan = change global_parsers (fn tab => |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
89 |
(if not (Symtab.defined tab name) then () |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
90 |
else warning ("Redefined ML antiquotation: " ^ quote name); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
91 |
Symtab.update (name, scan >> kind) tab)); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
92 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
93 |
in |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
94 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
95 |
val inline_antiq = add_item Inline; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
96 |
val value_antiq = add_item Value; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
97 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
98 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
99 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
100 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
101 |
(* command syntax *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
102 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
103 |
fun syntax scan src = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
104 |
#1 (Args.context_syntax "ML antiquotation" (Scan.lift scan) src (the_local_context ())); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
105 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
106 |
fun command src = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
107 |
let val ((name, _), pos) = Args.dest_src src in |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
108 |
(case Symtab.lookup (! global_parsers) name of |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
109 |
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
|
110 |
| SOME scan => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
111 |
(fn () => syntax scan src) ()) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
112 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
113 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
114 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
115 |
(* outer syntax *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
116 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
117 |
structure T = OuterLex; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
118 |
structure P = OuterParse; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
119 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
120 |
val antiq = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
121 |
P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
122 |
>> (fn ((x, pos), y) => Args.src ((x, y), pos)); |
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 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
125 |
(* input/output wrappers *) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
126 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
127 |
local |
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 isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;"; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
130 |
val isabelle_struct0 = isabelle_struct ""; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
131 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
132 |
fun eval_antiquotes txt = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
133 |
let |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
134 |
val ants = Antiquote.scan_antiquotes (txt, Position.line 1); |
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 expand (Antiquote.Text s) names = (("", Symbol.escape s), names) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
137 |
| expand (Antiquote.Antiq x) names = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
138 |
(case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
139 |
Inline s => (("", s), names) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
140 |
| Value (a, s) => |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
141 |
let |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
142 |
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
|
143 |
val ([b], names') = Name.variants [a'] names; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
144 |
in (("val " ^ b ^ " = " ^ s ^ ";\n", "Isabelle." ^ b), names') end); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
145 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
146 |
val (decls, body) = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
147 |
fold_map expand ants ML_Syntax.reserved |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
148 |
|> #1 |> split_list |> pairself implode; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
149 |
in (isabelle_struct decls, body) end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
150 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
151 |
fun eval verbose txt = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
152 |
Output.ML_errors (use_text Output.ml_output verbose) txt; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
153 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
154 |
in |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
155 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
156 |
fun eval_wrapper verbose txt = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
157 |
let val (txt1, txt2) = eval_antiquotes txt |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
158 |
in eval false txt1; eval verbose txt2; eval false isabelle_struct0 end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
159 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
160 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
161 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
162 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
163 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
164 |
(** ML evaluation **) |
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 |
fun use_mltext txt verbose opt_context = setmp opt_context (fn () => eval_wrapper verbose txt) (); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
167 |
fun use_mltext_update txt verbose context = #2 (pass_context context (eval_wrapper verbose) txt); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
168 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
169 |
fun use_context txt = use_mltext_update |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
170 |
("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
|
171 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
172 |
fun use_let bind body txt = |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
173 |
use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
174 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
175 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
176 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
177 |
(** implicit fact references **) |
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 thm name = ProofContext.get_thm (the_local_context ()) (Name name); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
180 |
fun thms name = ProofContext.get_thms (the_local_context ()) (Name name); |
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 |
val _ = value_antiq "thm" |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
183 |
(Args.name >> (fn s => (s, "ML_Context.thm " ^ ML_Syntax.print_string s))); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
184 |
val _ = value_antiq "thms" |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
185 |
(Args.name >> (fn s => (s, "ML_Context.thms " ^ ML_Syntax.print_string s))); |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
186 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
187 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
188 |
(*final declarations of this structure!*) |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
189 |
nonfix >>; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
190 |
fun >> f = change_theory f; |
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 |
end; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
193 |
|
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
194 |
structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context; |
ecdbab20c92c
ML context and antiquotations (material from context.ML);
wenzelm
parents:
diff
changeset
|
195 |
open Basic_ML_Context; |