author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 14954 | f1789e22ceec |
child 15144 | 85929e1b307d |
permissions | -rw-r--r-- |
5829 | 1 |
(* Title: Pure/Isar/outer_syntax.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
5 |
The global Isabelle/Isar outer syntax. |
|
6 |
*) |
|
7 |
||
8 |
signature BASIC_OUTER_SYNTAX = |
|
9 |
sig |
|
10 |
val main: unit -> unit |
|
5883 | 11 |
val loop: unit -> unit |
6860 | 12 |
val sync_main: unit -> unit |
13 |
val sync_loop: unit -> unit |
|
5829 | 14 |
end; |
15 |
||
16 |
signature OUTER_SYNTAX = |
|
17 |
sig |
|
18 |
include BASIC_OUTER_SYNTAX |
|
6722 | 19 |
structure Keyword: |
20 |
sig |
|
21 |
val control: string |
|
22 |
val diag: string |
|
23 |
val thy_begin: string |
|
7104 | 24 |
val thy_switch: string |
6722 | 25 |
val thy_end: string |
26 |
val thy_heading: string |
|
27 |
val thy_decl: string |
|
9588 | 28 |
val thy_script: string |
6722 | 29 |
val thy_goal: string |
30 |
val qed: string |
|
6733 | 31 |
val qed_block: string |
8209 | 32 |
val qed_global: string |
9552 | 33 |
val prf_heading: string |
6722 | 34 |
val prf_goal: string |
35 |
val prf_block: string |
|
9056 | 36 |
val prf_open: string |
37 |
val prf_close: string |
|
6722 | 38 |
val prf_chain: string |
39 |
val prf_decl: string |
|
6868 | 40 |
val prf_asm: string |
7676 | 41 |
val prf_asm_goal: string |
6722 | 42 |
val prf_script: string |
43 |
val kinds: string list |
|
44 |
end |
|
5829 | 45 |
type token |
46 |
type parser |
|
6722 | 47 |
val command: string -> string -> string -> |
6373 | 48 |
(token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser |
9132 | 49 |
val markup_command: IsarOutput.markup -> string -> string -> string -> |
7789 | 50 |
(token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser |
6722 | 51 |
val improper_command: string -> string -> string -> |
6373 | 52 |
(token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser |
14687 | 53 |
val is_keyword: string -> bool |
7026 | 54 |
val dest_keywords: unit -> string list |
55 |
val dest_parsers: unit -> (string * string * string * bool) list |
|
5883 | 56 |
val print_outer_syntax: unit -> unit |
9223 | 57 |
val print_commands: Toplevel.transition -> Toplevel.transition |
5829 | 58 |
val add_keywords: string list -> unit |
59 |
val add_parsers: parser list -> unit |
|
12943 | 60 |
val check_text: string * Position.T -> bool -> Toplevel.state -> unit |
7940 | 61 |
val deps_thy: string -> bool -> Path.T -> string list * Path.T list |
6199 | 62 |
val load_thy: string -> bool -> bool -> Path.T -> unit |
14091 | 63 |
val isar: bool -> bool -> unit Toplevel.isar |
64 |
val isar_readstring: Position.T -> string -> (string list) Toplevel.isar |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
65 |
val read: string -> (string * OuterLex.token list * Toplevel.transition) list |
5829 | 66 |
end; |
67 |
||
68 |
structure OuterSyntax: OUTER_SYNTAX = |
|
69 |
struct |
|
70 |
||
7750 | 71 |
structure T = OuterLex; |
6860 | 72 |
structure P = OuterParse; |
73 |
||
5829 | 74 |
|
75 |
(** outer syntax **) |
|
76 |
||
6722 | 77 |
(* command keyword classification *) |
78 |
||
79 |
structure Keyword = |
|
80 |
struct |
|
81 |
val control = "control"; |
|
82 |
val diag = "diag"; |
|
83 |
val thy_begin = "theory-begin"; |
|
7104 | 84 |
val thy_switch = "theory-switch"; |
6722 | 85 |
val thy_end = "theory-end"; |
86 |
val thy_heading = "theory-heading"; |
|
87 |
val thy_decl = "theory-decl"; |
|
9588 | 88 |
val thy_script = "theory-script"; |
6722 | 89 |
val thy_goal = "theory-goal"; |
90 |
val qed = "qed"; |
|
6733 | 91 |
val qed_block = "qed-block"; |
8209 | 92 |
val qed_global = "qed-global"; |
9552 | 93 |
val prf_heading = "proof-heading"; |
6722 | 94 |
val prf_goal = "proof-goal"; |
95 |
val prf_block = "proof-block"; |
|
9056 | 96 |
val prf_open = "proof-open"; |
97 |
val prf_close = "proof-close"; |
|
6722 | 98 |
val prf_chain = "proof-chain"; |
99 |
val prf_decl = "proof-decl"; |
|
6868 | 100 |
val prf_asm = "proof-asm"; |
7676 | 101 |
val prf_asm_goal = "proof-asm-goal"; |
6722 | 102 |
val prf_script = "proof-script"; |
103 |
||
9588 | 104 |
val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, |
105 |
thy_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close, |
|
106 |
prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]; |
|
6722 | 107 |
end; |
108 |
||
109 |
||
5829 | 110 |
(* parsers *) |
111 |
||
7750 | 112 |
type token = T.token; |
5829 | 113 |
type parser_fn = token list -> (Toplevel.transition -> Toplevel.transition) * token list; |
114 |
||
115 |
datatype parser = |
|
9132 | 116 |
Parser of string * (string * string * IsarOutput.markup option) * bool * parser_fn; |
5829 | 117 |
|
7750 | 118 |
fun parser int_only markup name comment kind parse = |
119 |
Parser (name, (comment, kind, markup), int_only, parse); |
|
5829 | 120 |
|
121 |
||
122 |
(* parse command *) |
|
123 |
||
6860 | 124 |
local |
6199 | 125 |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
126 |
fun terminate false = Scan.succeed () |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
127 |
| terminate true = P.group "end of input" (Scan.option P.sync -- P.semicolon >> K ()); |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
128 |
|
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
129 |
fun trace false parse = parse |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
130 |
| trace true parse = Scan.trace parse >> (fn (f, toks) => f o Toplevel.source toks); |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
131 |
|
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
132 |
fun body cmd trc (name, _) = |
7026 | 133 |
(case cmd name of |
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
134 |
Some (int_only, parse) => |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
135 |
P.!!! (Scan.prompt (name ^ "# ") (trace trc parse >> pair int_only)) |
7026 | 136 |
| None => sys_error ("no parser for outer syntax command " ^ quote name)); |
6860 | 137 |
|
138 |
in |
|
5829 | 139 |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
140 |
fun command do_terminate do_trace cmd = |
9132 | 141 |
P.semicolon >> K None || |
6860 | 142 |
P.sync >> K None || |
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
143 |
(P.position P.command :-- body cmd do_trace) --| terminate do_terminate |
6860 | 144 |
>> (fn ((name, pos), (int_only, f)) => |
145 |
Some (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |> |
|
146 |
Toplevel.interactive int_only |> f)); |
|
5829 | 147 |
|
6199 | 148 |
end; |
149 |
||
5829 | 150 |
|
151 |
||
9132 | 152 |
(** global outer syntax **) |
5829 | 153 |
|
7026 | 154 |
local |
155 |
||
156 |
val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon); |
|
7750 | 157 |
val global_parsers = |
9132 | 158 |
ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * IsarOutput.markup option) |
159 |
Symtab.table); |
|
160 |
val global_markups = ref ([]: (string * IsarOutput.markup) list); |
|
5952 | 161 |
|
7026 | 162 |
fun change_lexicons f = |
163 |
let val lexs = f (! global_lexicons) in |
|
164 |
(case (op inter_string) (pairself Scan.dest_lexicon lexs) of |
|
165 |
[] => global_lexicons := lexs |
|
166 |
| bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads)) |
|
167 |
end; |
|
5829 | 168 |
|
7789 | 169 |
fun get_markup (ms, (name, (_, Some m))) = (name, m) :: ms |
170 |
| get_markup (ms, _) = ms; |
|
7750 | 171 |
|
172 |
fun make_markups () = global_markups := Symtab.foldl get_markup ([], ! global_parsers); |
|
9132 | 173 |
fun change_parsers f = (Library.change global_parsers f; make_markups ()); |
6722 | 174 |
|
7026 | 175 |
in |
176 |
||
7750 | 177 |
|
9132 | 178 |
(* access current syntax *) |
7026 | 179 |
|
180 |
(*Note: the syntax for files is statically determined at the very |
|
181 |
beginning; for interactive processing it may change dynamically.*) |
|
182 |
||
183 |
fun get_lexicons () = ! global_lexicons; |
|
184 |
fun get_parsers () = ! global_parsers; |
|
7750 | 185 |
fun get_parser () = apsome (#2 o #1) o curry Symtab.lookup (! global_parsers); |
7789 | 186 |
|
9132 | 187 |
fun is_markup kind name = |
188 |
(case assoc (! global_markups, name) of Some k => k = kind | None => false); |
|
189 |
fun markup kind = Scan.one (T.is_kind T.Command andf is_markup kind o T.val_of); |
|
5829 | 190 |
|
191 |
||
192 |
(* augment syntax *) |
|
193 |
||
7026 | 194 |
fun add_keywords keywords = change_lexicons (apfst (fn lex => |
195 |
(Scan.extend_lexicon lex (map Symbol.explode keywords)))); |
|
5829 | 196 |
|
7750 | 197 |
fun add_parser (tab, Parser (name, (comment, kind, markup), int_only, parse)) = |
5829 | 198 |
(if is_none (Symtab.lookup (tab, name)) then () |
199 |
else warning ("Redefined outer syntax command " ^ quote name); |
|
7750 | 200 |
Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab)); |
5829 | 201 |
|
202 |
fun add_parsers parsers = |
|
7026 | 203 |
(change_parsers (fn tab => foldl add_parser (tab, parsers)); |
204 |
change_lexicons (apsnd (fn lex => Scan.extend_lexicon lex |
|
205 |
(map (fn Parser (name, _, _, _) => Symbol.explode name) parsers)))); |
|
206 |
||
207 |
end; |
|
5829 | 208 |
|
209 |
||
7026 | 210 |
(* print syntax *) |
211 |
||
14687 | 212 |
fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s); |
7026 | 213 |
fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ())); |
214 |
||
215 |
fun dest_parsers () = |
|
7750 | 216 |
map (fn (name, (((cmt, kind), (int_only, _)), _)) => (name, cmt, kind, int_only)) |
7026 | 217 |
(Symtab.dest (get_parsers ())); |
5829 | 218 |
|
9223 | 219 |
fun print_outer_syntax () = |
7026 | 220 |
let |
221 |
fun pretty_cmd (name, comment, _, _) = |
|
222 |
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; |
|
223 |
val (int_cmds, cmds) = partition #4 (dest_parsers ()); |
|
224 |
in |
|
8720 | 225 |
[Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())), |
226 |
Pretty.big_list "proper commands:" (map pretty_cmd cmds), |
|
227 |
Pretty.big_list "improper commands (interactive-only):" (map pretty_cmd int_cmds)] |
|
9223 | 228 |
|> Pretty.chunks |> Pretty.writeln |
7026 | 229 |
end; |
5829 | 230 |
|
9223 | 231 |
val print_commands = Toplevel.imperative print_outer_syntax; |
7367 | 232 |
|
5829 | 233 |
|
234 |
||
9132 | 235 |
(** toplevel parsing **) |
5829 | 236 |
|
9132 | 237 |
(* basic sources *) |
6860 | 238 |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
239 |
fun toplevel_source term trc do_recover cmd src = |
9132 | 240 |
let |
241 |
val no_terminator = |
|
242 |
Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof)); |
|
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
243 |
fun recover x = (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [None]) x; |
9132 | 244 |
in |
245 |
src |
|
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
246 |
|> T.source_proper |
9132 | 247 |
|> Source.source T.stopper |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
248 |
(Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K None || P.not_eof >> Some)) |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
249 |
(if do_recover then Some recover else None) |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
250 |
|> Source.mapfilter I |
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
251 |
|> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term trc (cmd ())) xs)) |
9132 | 252 |
(if do_recover then Some recover else None) |
253 |
|> Source.mapfilter I |
|
254 |
end; |
|
5829 | 255 |
|
7746 | 256 |
|
9132 | 257 |
(* interactive source of toplevel transformers *) |
5829 | 258 |
|
9132 | 259 |
fun isar term no_pos = |
260 |
Source.tty |
|
261 |
|> Symbol.source true |
|
262 |
|> T.source true get_lexicons |
|
263 |
(if no_pos then Position.none else Position.line_name 1 "stdin") |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
264 |
|> toplevel_source term false true get_parser; |
6199 | 265 |
|
266 |
||
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
267 |
(* string source of transformers with trace (for Proof General) *) |
14091 | 268 |
|
269 |
fun isar_readstring pos str = |
|
270 |
Source.of_string str |
|
271 |
|> Symbol.source false |
|
272 |
|> T.source false get_lexicons pos |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
273 |
|> toplevel_source false true true get_parser; |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
274 |
|
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
275 |
|
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
276 |
(* read text -- with trace of source *) |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
277 |
|
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
278 |
fun read str = |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
279 |
Source.of_string str |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
280 |
|> Symbol.source false |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
281 |
|> T.source false get_lexicons Position.none |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
282 |
|> toplevel_source false true true get_parser |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
283 |
|> Source.exhaust |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
284 |
|> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr)); |
14091 | 285 |
|
286 |
||
7746 | 287 |
|
9132 | 288 |
(** read theory **) |
6247 | 289 |
|
12943 | 290 |
(* check_text *) |
291 |
||
292 |
fun check_text s true state = (IsarOutput.eval_antiquote (#1 (get_lexicons ())) state s; ()) |
|
293 |
| check_text _ false _ = (); |
|
294 |
||
295 |
||
9132 | 296 |
(* deps_thy *) |
6199 | 297 |
|
7940 | 298 |
fun deps_thy name ml path = |
6199 | 299 |
let |
7735 | 300 |
val src = Source.of_string (File.read path); |
301 |
val pos = Path.position path; |
|
9132 | 302 |
val (name', parents, files) = ThyHeader.scan (src, pos); |
6199 | 303 |
val ml_path = ThyLoad.ml_path name; |
7940 | 304 |
val ml_file = if ml andalso is_some (ThyLoad.check_file ml_path) then [ml_path] else []; |
6199 | 305 |
in |
306 |
if name <> name' then |
|
7940 | 307 |
error ("Filename " ^ quote (Path.pack path) ^ |
8078 | 308 |
" does not agree with theory name " ^ quote name') |
6247 | 309 |
else (parents, map (Path.unpack o #1) files @ ml_file) |
6199 | 310 |
end; |
311 |
||
7746 | 312 |
|
9132 | 313 |
(* load_thy *) |
6199 | 314 |
|
7746 | 315 |
local |
316 |
||
7940 | 317 |
fun try_ml_file name time = |
6199 | 318 |
let |
319 |
val path = ThyLoad.ml_path name; |
|
7940 | 320 |
val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path); |
6247 | 321 |
val tr_name = if time then "time_use" else "use"; |
6199 | 322 |
in |
7243 | 323 |
if is_none (ThyLoad.check_file path) then () |
9132 | 324 |
else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] |
6199 | 325 |
end; |
326 |
||
9132 | 327 |
fun parse_thy src = |
328 |
src |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
329 |
|> toplevel_source false false false (K (get_parser ())) |
7746 | 330 |
|> Source.exhaust; |
5829 | 331 |
|
6247 | 332 |
fun run_thy name path = |
7683 | 333 |
let |
7735 | 334 |
val pos = Path.position path; |
9132 | 335 |
val text = Library.untabify (explode (File.read path)); |
336 |
val text_src = Source.of_list text; |
|
337 |
fun present_text () = Source.exhaust (Symbol.source false text_src); |
|
7683 | 338 |
in |
7735 | 339 |
Present.init_theory name; |
9132 | 340 |
Present.verbatim_source name present_text; |
341 |
if ThyHeader.is_old (text_src, pos) then (ThySyn.load_thy name text; |
|
342 |
Present.old_symbol_source name present_text) (*note: text presented twice*) |
|
343 |
else |
|
344 |
let |
|
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
345 |
val tok_src = text_src |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
346 |
|> Symbol.source false |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
347 |
|> T.source false (K (get_lexicons ())) pos |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
348 |
|> Source.exhausted; |
9132 | 349 |
val out = Toplevel.excursion_result |
350 |
(IsarOutput.parse_thy markup (#1 (get_lexicons ())) |
|
351 |
(parse_thy tok_src) tok_src); |
|
352 |
in Present.theory_output name (Buffer.content out) end |
|
6247 | 353 |
end; |
6199 | 354 |
|
7746 | 355 |
in |
356 |
||
6199 | 357 |
fun load_thy name ml time path = |
6247 | 358 |
(if time then |
359 |
timeit (fn () => |
|
360 |
(writeln ("\n**** Starting theory " ^ quote name ^ " ****"); |
|
9036 | 361 |
run_thy name path; |
6247 | 362 |
writeln ("**** Finished theory " ^ quote name ^ " ****\n"))) |
363 |
else run_thy name path; |
|
364 |
Context.context (ThyInfo.get_theory name); |
|
7940 | 365 |
if ml then try_ml_file name time else ()); |
5829 | 366 |
|
7746 | 367 |
end; |
368 |
||
5829 | 369 |
|
370 |
||
371 |
(** the read-eval-print loop **) |
|
372 |
||
5923 | 373 |
(* main loop *) |
374 |
||
7333 | 375 |
fun gen_loop term no_pos = |
376 |
(Context.reset_context (); |
|
377 |
Toplevel.loop (isar term no_pos)); |
|
5829 | 378 |
|
7333 | 379 |
fun gen_main term no_pos = |
5829 | 380 |
(Toplevel.set_state Toplevel.toplevel; |
6199 | 381 |
writeln (Session.welcome ()); |
7333 | 382 |
gen_loop term no_pos); |
6860 | 383 |
|
7333 | 384 |
fun main () = gen_main false false; |
385 |
fun loop () = gen_loop false false; |
|
386 |
fun sync_main () = gen_main true true; |
|
387 |
fun sync_loop () = gen_loop true true; |
|
5829 | 388 |
|
389 |
||
6373 | 390 |
(*final declarations of this structure!*) |
7789 | 391 |
val command = parser false None; |
9132 | 392 |
val markup_command = parser false o Some; |
7789 | 393 |
val improper_command = parser true None; |
6685 | 394 |
|
6373 | 395 |
|
5829 | 396 |
end; |
397 |
||
6199 | 398 |
(*setup theory syntax dependent operations*) |
399 |
ThyLoad.deps_thy_fn := OuterSyntax.deps_thy; |
|
400 |
ThyLoad.load_thy_fn := OuterSyntax.load_thy; |
|
401 |
structure ThyLoad: THY_LOAD = ThyLoad; |
|
402 |
||
5829 | 403 |
structure BasicOuterSyntax: BASIC_OUTER_SYNTAX = OuterSyntax; |
404 |
open BasicOuterSyntax; |