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