author | wenzelm |
Mon, 05 Sep 2005 17:38:23 +0200 | |
changeset 17265 | 12d99bb4304b |
parent 17250 | 158ef530c153 |
child 17283 | 881f5873bac0 |
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 |
|
15830 | 10 |
structure Isar: |
11 |
sig |
|
12 |
val main: unit -> unit |
|
13 |
val loop: unit -> unit |
|
14 |
val sync_main: unit -> unit |
|
15 |
val sync_loop: unit -> unit |
|
16 |
end; |
|
5829 | 17 |
end; |
18 |
||
19 |
signature OUTER_SYNTAX = |
|
20 |
sig |
|
21 |
include BASIC_OUTER_SYNTAX |
|
22 |
type token |
|
23 |
type parser |
|
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
24 |
val command: string -> string -> OuterKeyword.T -> |
6373 | 25 |
(token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser |
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
26 |
val markup_command: IsarOutput.markup -> string -> string -> OuterKeyword.T -> |
7789 | 27 |
(token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser |
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
28 |
val improper_command: string -> string -> OuterKeyword.T -> |
6373 | 29 |
(token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser |
14687 | 30 |
val is_keyword: string -> bool |
7026 | 31 |
val dest_keywords: unit -> string list |
32 |
val dest_parsers: unit -> (string * string * string * bool) list |
|
5883 | 33 |
val print_outer_syntax: unit -> unit |
9223 | 34 |
val print_commands: Toplevel.transition -> Toplevel.transition |
5829 | 35 |
val add_keywords: string list -> unit |
36 |
val add_parsers: parser list -> unit |
|
17265 | 37 |
val check_text: string * Position.T -> Toplevel.state -> unit |
7940 | 38 |
val deps_thy: string -> bool -> Path.T -> string list * Path.T list |
6199 | 39 |
val load_thy: string -> bool -> bool -> Path.T -> unit |
14091 | 40 |
val isar: bool -> bool -> unit Toplevel.isar |
16195 | 41 |
val scan: string -> OuterLex.token list |
42 |
val read: OuterLex.token list -> (string * OuterLex.token list * Toplevel.transition) list |
|
5829 | 43 |
end; |
44 |
||
15224
1bd35fd87963
Allow scanning to recover and reconstruct bad input
aspinall
parents:
15156
diff
changeset
|
45 |
structure OuterSyntax : OUTER_SYNTAX = |
5829 | 46 |
struct |
47 |
||
7750 | 48 |
structure T = OuterLex; |
6860 | 49 |
structure P = OuterParse; |
50 |
||
5829 | 51 |
|
52 |
(** outer syntax **) |
|
53 |
||
54 |
(* parsers *) |
|
55 |
||
7750 | 56 |
type token = T.token; |
5829 | 57 |
type parser_fn = token list -> (Toplevel.transition -> Toplevel.transition) * token list; |
58 |
||
59 |
datatype parser = |
|
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
60 |
Parser of string * (string * OuterKeyword.T * IsarOutput.markup option) * bool * parser_fn; |
5829 | 61 |
|
7750 | 62 |
fun parser int_only markup name comment kind parse = |
63 |
Parser (name, (comment, kind, markup), int_only, parse); |
|
5829 | 64 |
|
65 |
||
66 |
(* parse command *) |
|
67 |
||
6860 | 68 |
local |
6199 | 69 |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
70 |
fun terminate false = Scan.succeed () |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
71 |
| 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
|
72 |
|
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
73 |
fun trace false parse = parse |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
74 |
| 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
|
75 |
|
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
76 |
fun body cmd do_trace (name, _) = |
7026 | 77 |
(case cmd name of |
15531 | 78 |
SOME (int_only, parse) => |
17118 | 79 |
P.!!! (Scan.prompt (name ^ "# ") (trace do_trace (P.tags |-- parse) >> pair int_only)) |
15531 | 80 |
| NONE => sys_error ("no parser for outer syntax command " ^ quote name)); |
6860 | 81 |
|
82 |
in |
|
5829 | 83 |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
84 |
fun command do_terminate do_trace cmd = |
15531 | 85 |
P.semicolon >> K NONE || |
86 |
P.sync >> K NONE || |
|
17118 | 87 |
(P.position P.command :-- body cmd do_trace) --| terminate do_terminate |
6860 | 88 |
>> (fn ((name, pos), (int_only, f)) => |
15531 | 89 |
SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |> |
6860 | 90 |
Toplevel.interactive int_only |> f)); |
5829 | 91 |
|
6199 | 92 |
end; |
93 |
||
5829 | 94 |
|
95 |
||
9132 | 96 |
(** global outer syntax **) |
5829 | 97 |
|
7026 | 98 |
local |
99 |
||
100 |
val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon); |
|
7750 | 101 |
val global_parsers = |
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
102 |
ref (Symtab.empty: (((string * OuterKeyword.T) * (bool * parser_fn)) * IsarOutput.markup option) |
9132 | 103 |
Symtab.table); |
104 |
val global_markups = ref ([]: (string * IsarOutput.markup) list); |
|
5952 | 105 |
|
7026 | 106 |
fun change_lexicons f = |
107 |
let val lexs = f (! global_lexicons) in |
|
108 |
(case (op inter_string) (pairself Scan.dest_lexicon lexs) of |
|
109 |
[] => global_lexicons := lexs |
|
110 |
| bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads)) |
|
111 |
end; |
|
5829 | 112 |
|
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
113 |
fun make_markups () = global_markups := |
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
114 |
Symtab.fold (fn (name, (_, SOME m)) => cons (name, m) | _ => I) (! global_parsers) []; |
7750 | 115 |
|
9132 | 116 |
fun change_parsers f = (Library.change global_parsers f; make_markups ()); |
6722 | 117 |
|
7026 | 118 |
in |
119 |
||
7750 | 120 |
|
9132 | 121 |
(* access current syntax *) |
7026 | 122 |
|
123 |
(*Note: the syntax for files is statically determined at the very |
|
124 |
beginning; for interactive processing it may change dynamically.*) |
|
125 |
||
126 |
fun get_lexicons () = ! global_lexicons; |
|
127 |
fun get_parsers () = ! global_parsers; |
|
17221 | 128 |
fun get_parser () = Option.map (#2 o #1) o Symtab.curried_lookup (get_parsers ()); |
7789 | 129 |
|
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
130 |
fun command_tags name = |
17221 | 131 |
(case Symtab.curried_lookup (get_parsers ()) name of |
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
132 |
SOME (((_, k), _), _) => OuterKeyword.tags_of k |
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
133 |
| NONE => []); |
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
134 |
|
17184 | 135 |
fun is_markup kind name = (AList.lookup (op =) (! global_markups) name = SOME kind); |
5829 | 136 |
|
137 |
||
138 |
(* augment syntax *) |
|
139 |
||
7026 | 140 |
fun add_keywords keywords = change_lexicons (apfst (fn lex => |
141 |
(Scan.extend_lexicon lex (map Symbol.explode keywords)))); |
|
5829 | 142 |
|
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
143 |
fun add_parser (Parser (name, (comment, kind, markup), int_only, parse)) tab = |
16894 | 144 |
(if not (Symtab.defined tab name) then () |
5829 | 145 |
else warning ("Redefined outer syntax command " ^ quote name); |
17221 | 146 |
Symtab.curried_update (name, (((comment, kind), (int_only, parse)), markup)) tab); |
5829 | 147 |
|
148 |
fun add_parsers parsers = |
|
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
149 |
(change_parsers (fold add_parser parsers); |
7026 | 150 |
change_lexicons (apsnd (fn lex => Scan.extend_lexicon lex |
151 |
(map (fn Parser (name, _, _, _) => Symbol.explode name) parsers)))); |
|
152 |
||
153 |
end; |
|
5829 | 154 |
|
155 |
||
7026 | 156 |
(* print syntax *) |
157 |
||
14687 | 158 |
fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s); |
7026 | 159 |
fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ())); |
160 |
||
161 |
fun dest_parsers () = |
|
16727 | 162 |
get_parsers () |> Symtab.dest |> sort_wrt #1 |
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
163 |
|> map (fn (name, (((cmt, kind), (int_only, _)), _)) => |
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
164 |
(name, cmt, OuterKeyword.kind_of kind, int_only)); |
5829 | 165 |
|
9223 | 166 |
fun print_outer_syntax () = |
7026 | 167 |
let |
168 |
fun pretty_cmd (name, comment, _, _) = |
|
169 |
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; |
|
15570 | 170 |
val (int_cmds, cmds) = List.partition #4 (dest_parsers ()); |
7026 | 171 |
in |
8720 | 172 |
[Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())), |
173 |
Pretty.big_list "proper commands:" (map pretty_cmd cmds), |
|
174 |
Pretty.big_list "improper commands (interactive-only):" (map pretty_cmd int_cmds)] |
|
9223 | 175 |
|> Pretty.chunks |> Pretty.writeln |
7026 | 176 |
end; |
5829 | 177 |
|
9223 | 178 |
val print_commands = Toplevel.imperative print_outer_syntax; |
7367 | 179 |
|
5829 | 180 |
|
181 |
||
9132 | 182 |
(** toplevel parsing **) |
5829 | 183 |
|
9132 | 184 |
(* basic sources *) |
6860 | 185 |
|
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
186 |
fun toplevel_source term do_trace do_recover cmd src = |
9132 | 187 |
let |
188 |
val no_terminator = |
|
189 |
Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof)); |
|
15531 | 190 |
fun recover x = (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]) x; |
9132 | 191 |
in |
192 |
src |
|
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
193 |
|> T.source_proper |
9132 | 194 |
|> Source.source T.stopper |
15531 | 195 |
(Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME)) |
196 |
(if do_recover then SOME recover else NONE) |
|
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
197 |
|> Source.mapfilter I |
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
198 |
|> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term do_trace (cmd ())) xs)) |
15531 | 199 |
(if do_recover then SOME recover else NONE) |
9132 | 200 |
|> Source.mapfilter I |
201 |
end; |
|
5829 | 202 |
|
7746 | 203 |
|
9132 | 204 |
(* interactive source of toplevel transformers *) |
5829 | 205 |
|
9132 | 206 |
fun isar term no_pos = |
207 |
Source.tty |
|
208 |
|> Symbol.source true |
|
209 |
|> T.source true get_lexicons |
|
210 |
(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
|
211 |
|> toplevel_source term false true get_parser; |
6199 | 212 |
|
213 |
||
16195 | 214 |
(* scan text *) |
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
215 |
|
15144
85929e1b307d
Remove isar_readstring. Split read into scanner and parser.
aspinall
parents:
14981
diff
changeset
|
216 |
fun scan str = |
16195 | 217 |
Source.of_string str |
218 |
|> Symbol.source false |
|
219 |
|> T.source true get_lexicons Position.none |
|
220 |
|> Source.exhaust; |
|
221 |
||
222 |
||
223 |
(* read tokens with trace *) |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
224 |
|
15144
85929e1b307d
Remove isar_readstring. Split read into scanner and parser.
aspinall
parents:
14981
diff
changeset
|
225 |
fun read toks = |
85929e1b307d
Remove isar_readstring. Split read into scanner and parser.
aspinall
parents:
14981
diff
changeset
|
226 |
Source.of_list toks |
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
227 |
|> toplevel_source false true true get_parser |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
228 |
|> Source.exhaust |
15973 | 229 |
|> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr)); |
14091 | 230 |
|
231 |
||
16195 | 232 |
|
9132 | 233 |
(** read theory **) |
6247 | 234 |
|
12943 | 235 |
(* check_text *) |
236 |
||
17265 | 237 |
fun check_text s state = (IsarOutput.eval_antiquote (#1 (get_lexicons ())) state s; ()); |
12943 | 238 |
|
239 |
||
9132 | 240 |
(* deps_thy *) |
6199 | 241 |
|
7940 | 242 |
fun deps_thy name ml path = |
6199 | 243 |
let |
7735 | 244 |
val src = Source.of_string (File.read path); |
245 |
val pos = Path.position path; |
|
9132 | 246 |
val (name', parents, files) = ThyHeader.scan (src, pos); |
6199 | 247 |
val ml_path = ThyLoad.ml_path name; |
15973 | 248 |
val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else []; |
6199 | 249 |
in |
250 |
if name <> name' then |
|
7940 | 251 |
error ("Filename " ^ quote (Path.pack path) ^ |
8078 | 252 |
" does not agree with theory name " ^ quote name') |
6247 | 253 |
else (parents, map (Path.unpack o #1) files @ ml_file) |
6199 | 254 |
end; |
255 |
||
7746 | 256 |
|
9132 | 257 |
(* load_thy *) |
6199 | 258 |
|
7746 | 259 |
local |
260 |
||
7940 | 261 |
fun try_ml_file name time = |
6199 | 262 |
let |
263 |
val path = ThyLoad.ml_path name; |
|
7940 | 264 |
val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path); |
6247 | 265 |
val tr_name = if time then "time_use" else "use"; |
6199 | 266 |
in |
15531 | 267 |
if is_none (ThyLoad.check_file NONE path) then () |
9132 | 268 |
else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] |
6199 | 269 |
end; |
270 |
||
6247 | 271 |
fun run_thy name path = |
7683 | 272 |
let |
7735 | 273 |
val pos = Path.position path; |
9132 | 274 |
val text = Library.untabify (explode (File.read path)); |
275 |
val text_src = Source.of_list text; |
|
276 |
fun present_text () = Source.exhaust (Symbol.source false text_src); |
|
7683 | 277 |
in |
7735 | 278 |
Present.init_theory name; |
9132 | 279 |
Present.verbatim_source name present_text; |
17237 | 280 |
if ThyHeader.is_old (text_src, pos) then |
17250 | 281 |
(warning ("Non-Isar file format for theory " ^ quote name ^ " (deprecated)"); |
17237 | 282 |
ThySyn.load_thy name text; |
9132 | 283 |
Present.old_symbol_source name present_text) (*note: text presented twice*) |
284 |
else |
|
285 |
let |
|
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
286 |
val tok_src = text_src |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
287 |
|> Symbol.source false |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
288 |
|> T.source false (K (get_lexicons ())) pos |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
289 |
|> Source.exhausted; |
17071
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
290 |
val trs = |
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
291 |
tok_src |
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
292 |
|> toplevel_source false false false (K (get_parser ())) |
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
293 |
|> Source.exhaust; |
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
294 |
in |
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
295 |
IsarOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs tok_src |
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
296 |
|> Buffer.content |
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
297 |
|> Present.theory_output name |
f753d6dd9bd0
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
wenzelm
parents:
16894
diff
changeset
|
298 |
end |
6247 | 299 |
end; |
6199 | 300 |
|
7746 | 301 |
in |
302 |
||
6199 | 303 |
fun load_thy name ml time path = |
6247 | 304 |
(if time then |
305 |
timeit (fn () => |
|
306 |
(writeln ("\n**** Starting theory " ^ quote name ^ " ****"); |
|
9036 | 307 |
run_thy name path; |
6247 | 308 |
writeln ("**** Finished theory " ^ quote name ^ " ****\n"))) |
309 |
else run_thy name path; |
|
310 |
Context.context (ThyInfo.get_theory name); |
|
7940 | 311 |
if ml then try_ml_file name time else ()); |
5829 | 312 |
|
7746 | 313 |
end; |
314 |
||
5829 | 315 |
|
316 |
||
317 |
(** the read-eval-print loop **) |
|
318 |
||
5923 | 319 |
(* main loop *) |
320 |
||
7333 | 321 |
fun gen_loop term no_pos = |
322 |
(Context.reset_context (); |
|
15989 | 323 |
Toplevel.loop (isar term no_pos); |
324 |
ml_prompts "ML> " "ML# "); |
|
5829 | 325 |
|
7333 | 326 |
fun gen_main term no_pos = |
5829 | 327 |
(Toplevel.set_state Toplevel.toplevel; |
6199 | 328 |
writeln (Session.welcome ()); |
7333 | 329 |
gen_loop term no_pos); |
6860 | 330 |
|
15830 | 331 |
structure Isar = |
332 |
struct |
|
333 |
fun main () = gen_main false false; |
|
334 |
fun loop () = gen_loop false false; |
|
335 |
fun sync_main () = gen_main true true; |
|
336 |
fun sync_loop () = gen_loop true true; |
|
337 |
end; |
|
5829 | 338 |
|
339 |
||
6373 | 340 |
(*final declarations of this structure!*) |
15531 | 341 |
val command = parser false NONE; |
342 |
val markup_command = parser false o SOME; |
|
343 |
val improper_command = parser true NONE; |
|
6685 | 344 |
|
5829 | 345 |
end; |
346 |
||
6199 | 347 |
(*setup theory syntax dependent operations*) |
348 |
ThyLoad.deps_thy_fn := OuterSyntax.deps_thy; |
|
349 |
ThyLoad.load_thy_fn := OuterSyntax.load_thy; |
|
350 |
structure ThyLoad: THY_LOAD = ThyLoad; |
|
351 |
||
5829 | 352 |
structure BasicOuterSyntax: BASIC_OUTER_SYNTAX = OuterSyntax; |
353 |
open BasicOuterSyntax; |
|
15830 | 354 |
open Isar; |