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