author | wenzelm |
Tue, 15 Jul 2008 22:37:58 +0200 | |
changeset 27614 | f38c25d106a7 |
parent 27575 | e540ad3fb50a |
child 27720 | c8a462f1f4a2 |
permissions | -rw-r--r-- |
5829 | 1 |
(* Title: Pure/Isar/outer_syntax.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
5 |
The global Isabelle/Isar outer syntax. |
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
6 |
|
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
7 |
Note: the syntax for files is statically determined at the very |
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
8 |
beginning; for interactive processing it may change dynamically. |
5829 | 9 |
*) |
10 |
||
11 |
signature OUTER_SYNTAX = |
|
12 |
sig |
|
24868 | 13 |
type parser_fn = OuterLex.token list -> |
14 |
(Toplevel.transition -> Toplevel.transition) * OuterLex.token list |
|
15 |
val command: string -> string -> OuterKeyword.T -> parser_fn -> unit |
|
16 |
val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T -> parser_fn -> unit |
|
17 |
val improper_command: string -> string -> OuterKeyword.T -> parser_fn -> unit |
|
26990 | 18 |
val local_theory: string -> string -> OuterKeyword.T -> |
19 |
(OuterParse.token list -> (local_theory -> local_theory) * OuterLex.token list) -> unit |
|
20 |
val local_theory_to_proof': string -> string -> OuterKeyword.T -> |
|
21 |
(OuterParse.token list -> (bool -> local_theory -> Proof.state) * OuterLex.token list) -> unit |
|
22 |
val local_theory_to_proof: string -> string -> OuterKeyword.T -> |
|
23 |
(OuterParse.token list -> (local_theory -> Proof.state) * OuterLex.token list) -> unit |
|
5883 | 24 |
val print_outer_syntax: unit -> unit |
16195 | 25 |
val scan: string -> OuterLex.token list |
25580 | 26 |
val parse: Position.T -> string -> Toplevel.transition list |
27614
f38c25d106a7
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents:
27575
diff
changeset
|
27 |
val prepare_command: Markup.property list -> string * Position.T -> Toplevel.transition |
26431 | 28 |
val process_file: Path.T -> theory -> theory |
26600 | 29 |
type isar |
30 |
val isar: bool -> isar |
|
26611 | 31 |
val load_thy: Path.T -> string -> Position.T -> string list -> bool -> unit |
5829 | 32 |
end; |
33 |
||
26600 | 34 |
structure OuterSyntax: OUTER_SYNTAX = |
5829 | 35 |
struct |
36 |
||
7750 | 37 |
structure T = OuterLex; |
6860 | 38 |
structure P = OuterParse; |
39 |
||
5829 | 40 |
|
41 |
(** outer syntax **) |
|
42 |
||
43 |
(* parsers *) |
|
44 |
||
24868 | 45 |
type parser_fn = T.token list -> (Toplevel.transition -> Toplevel.transition) * T.token list; |
5829 | 46 |
|
24868 | 47 |
datatype parser = Parser of |
48 |
{comment: string, |
|
49 |
markup: ThyOutput.markup option, |
|
50 |
int_only: bool, |
|
51 |
parse: parser_fn}; |
|
5829 | 52 |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
53 |
fun make_parser comment markup int_only parse = |
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
54 |
Parser {comment = comment, markup = markup, int_only = int_only, parse = parse}; |
5829 | 55 |
|
56 |
||
57 |
(* parse command *) |
|
58 |
||
6860 | 59 |
local |
6199 | 60 |
|
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
61 |
fun terminate false = Scan.succeed () |
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
62 |
| 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
|
63 |
|
26620 | 64 |
fun body cmd (name, _) = |
7026 | 65 |
(case cmd name of |
24868 | 66 |
SOME (Parser {int_only, parse, ...}) => |
26620 | 67 |
P.!!! (Scan.prompt (name ^ "# ") (P.tags |-- parse >> pair int_only)) |
15531 | 68 |
| NONE => sys_error ("no parser for outer syntax command " ^ quote name)); |
6860 | 69 |
|
70 |
in |
|
5829 | 71 |
|
26620 | 72 |
fun parse_command do_terminate cmd = |
15531 | 73 |
P.semicolon >> K NONE || |
74 |
P.sync >> K NONE || |
|
26620 | 75 |
(P.position P.command :-- body cmd) --| terminate do_terminate |
6860 | 76 |
>> (fn ((name, pos), (int_only, f)) => |
15531 | 77 |
SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |> |
6860 | 78 |
Toplevel.interactive int_only |> f)); |
5829 | 79 |
|
6199 | 80 |
end; |
81 |
||
5829 | 82 |
|
83 |
||
9132 | 84 |
(** global outer syntax **) |
5829 | 85 |
|
7026 | 86 |
local |
87 |
||
24868 | 88 |
val global_parsers = ref (Symtab.empty: parser Symtab.table); |
22120 | 89 |
val global_markups = ref ([]: (string * ThyOutput.markup) list); |
5952 | 90 |
|
23939 | 91 |
fun change_parsers f = CRITICAL (fn () => |
92 |
(change global_parsers f; |
|
93 |
global_markups := |
|
24868 | 94 |
Symtab.fold (fn (name, Parser {markup = SOME m, ...}) => cons (name, m) | _ => I) |
95 |
(! global_parsers) [])); |
|
6722 | 96 |
|
7026 | 97 |
in |
98 |
||
9132 | 99 |
(* access current syntax *) |
7026 | 100 |
|
24868 | 101 |
fun get_parsers () = CRITICAL (fn () => ! global_parsers); |
102 |
fun get_markups () = CRITICAL (fn () => ! global_markups); |
|
7026 | 103 |
|
24868 | 104 |
fun get_parser () = Symtab.lookup (get_parsers ()); |
7789 | 105 |
|
24868 | 106 |
fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind; |
5829 | 107 |
|
108 |
||
109 |
(* augment syntax *) |
|
110 |
||
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
111 |
fun add_parser name kind parser = CRITICAL (fn () => |
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
112 |
(OuterKeyword.command name kind; |
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
113 |
if not (Symtab.defined (get_parsers ()) name) then () |
24868 | 114 |
else warning ("Redefining outer syntax command " ^ quote name); |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
115 |
change_parsers (Symtab.update (name, parser)))); |
5829 | 116 |
|
24868 | 117 |
fun command name comment kind parse = |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
118 |
add_parser name kind (make_parser comment NONE false parse); |
5829 | 119 |
|
24868 | 120 |
fun markup_command markup name comment kind parse = |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
121 |
add_parser name kind (make_parser comment (SOME markup) false parse); |
24868 | 122 |
|
123 |
fun improper_command name comment kind parse = |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
124 |
add_parser name kind (make_parser comment NONE true parse); |
7026 | 125 |
|
126 |
end; |
|
5829 | 127 |
|
128 |
||
26990 | 129 |
(* local_theory commands *) |
130 |
||
131 |
fun local_theory_command do_print trans name comment kind parse = |
|
132 |
command name comment kind (P.opt_target -- parse |
|
133 |
>> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f)); |
|
134 |
||
135 |
val local_theory = local_theory_command false Toplevel.local_theory; |
|
136 |
val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof'; |
|
137 |
val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof; |
|
138 |
||
139 |
||
24872 | 140 |
(* inspect syntax *) |
7026 | 141 |
|
142 |
fun dest_parsers () = |
|
16727 | 143 |
get_parsers () |> Symtab.dest |> sort_wrt #1 |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
144 |
|> map (fn (name, Parser {comment, int_only, ...}) => (name, comment, int_only)); |
5829 | 145 |
|
9223 | 146 |
fun print_outer_syntax () = |
7026 | 147 |
let |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
148 |
fun pretty_cmd (name, comment, _) = |
7026 | 149 |
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
150 |
val (int_cmds, cmds) = List.partition #3 (dest_parsers ()); |
7026 | 151 |
in |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
152 |
[Pretty.strs ("syntax keywords:" :: map quote (OuterKeyword.dest_keywords ())), |
18326 | 153 |
Pretty.big_list "commands:" (map pretty_cmd cmds), |
154 |
Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)] |
|
9223 | 155 |
|> Pretty.chunks |> Pretty.writeln |
7026 | 156 |
end; |
5829 | 157 |
|
158 |
||
159 |
||
9132 | 160 |
(** toplevel parsing **) |
5829 | 161 |
|
9132 | 162 |
(* basic sources *) |
6860 | 163 |
|
26620 | 164 |
fun toplevel_source term do_recover cmd src = |
9132 | 165 |
let |
166 |
val no_terminator = |
|
167 |
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
|
168 |
fun recover int = |
cf4773532006
nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents:
23679
diff
changeset
|
169 |
(int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]); |
9132 | 170 |
in |
171 |
src |
|
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
10749
diff
changeset
|
172 |
|> T.source_proper |
9132 | 173 |
|> Source.source T.stopper |
15531 | 174 |
(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
|
175 |
(Option.map recover do_recover) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19060
diff
changeset
|
176 |
|> Source.map_filter I |
24868 | 177 |
|> Source.source T.stopper |
26620 | 178 |
(Scan.bulk (fn xs => P.!!! (parse_command term (cmd ())) xs)) |
23682
cf4773532006
nested source: explicit interactive flag for recover avoids duplicate errors;
wenzelm
parents:
23679
diff
changeset
|
179 |
(Option.map recover do_recover) |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19060
diff
changeset
|
180 |
|> Source.map_filter I |
9132 | 181 |
end; |
5829 | 182 |
|
7746 | 183 |
|
25580 | 184 |
(* off-line scanning/parsing *) |
14925
0f86a8a694f8
added read (provides transition names and sources);
wenzelm
parents:
14687
diff
changeset
|
185 |
|
15144
85929e1b307d
Remove isar_readstring. Split read into scanner and parser.
aspinall
parents:
14981
diff
changeset
|
186 |
fun scan str = |
16195 | 187 |
Source.of_string str |
188 |
|> Symbol.source false |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
189 |
|> T.source (SOME false) OuterKeyword.get_lexicons Position.none |
16195 | 190 |
|> Source.exhaust; |
191 |
||
25580 | 192 |
fun parse pos str = |
193 |
Source.of_string str |
|
194 |
|> Symbol.source false |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
195 |
|> T.source (SOME false) OuterKeyword.get_lexicons pos |
26620 | 196 |
|> toplevel_source false NONE get_parser |
25580 | 197 |
|> Source.exhaust; |
198 |
||
27614
f38c25d106a7
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents:
27575
diff
changeset
|
199 |
fun prepare_command props (str, pos) = |
f38c25d106a7
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents:
27575
diff
changeset
|
200 |
let val pos' = Position.of_properties (props |> Position.default_properties pos) in |
f38c25d106a7
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents:
27575
diff
changeset
|
201 |
(case parse pos' str of |
f38c25d106a7
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents:
27575
diff
changeset
|
202 |
[transition] => transition |
f38c25d106a7
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents:
27575
diff
changeset
|
203 |
| _ => error "exactly one command expected") |
f38c25d106a7
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents:
27575
diff
changeset
|
204 |
end; |
f38c25d106a7
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents:
27575
diff
changeset
|
205 |
|
14091 | 206 |
|
26431 | 207 |
(* process file *) |
208 |
||
209 |
fun process_file path thy = |
|
210 |
let |
|
211 |
val result = ref thy; |
|
26881 | 212 |
val trs = parse (Path.position path) (File.read path); |
27575 | 213 |
val init = Toplevel.init_theory "" (K thy) (fn thy' => result := thy'); |
26431 | 214 |
val _ = Toplevel.excursion (init Toplevel.empty :: trs @ [Toplevel.exit Toplevel.empty]); |
215 |
in ! result end; |
|
216 |
||
217 |
||
24868 | 218 |
(* interactive source of toplevel transformers *) |
219 |
||
26600 | 220 |
type isar = |
221 |
(Toplevel.transition, (Toplevel.transition option, |
|
222 |
(OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token, |
|
223 |
Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source) |
|
224 |
Source.source) Source.source) Source.source) Source.source) Source.source) Source.source; |
|
225 |
||
226 |
fun isar term : isar = |
|
24868 | 227 |
Source.tty |
228 |
|> Symbol.source true |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
229 |
|> T.source (SOME true) OuterKeyword.get_lexicons Position.none |
26620 | 230 |
|> toplevel_source term (SOME true) get_parser; |
24868 | 231 |
|
232 |
||
26611 | 233 |
(* load_thy *) |
7746 | 234 |
|
26323
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26291
diff
changeset
|
235 |
fun load_thy dir name pos text time = |
7683 | 236 |
let |
24065 | 237 |
val text_src = Source.of_list (Library.untabify text); |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
238 |
val (lexs, parser) = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_parser ())); |
23866
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset
|
239 |
|
17932 | 240 |
val _ = Present.init_theory name; |
24065 | 241 |
val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text_src)); |
242 |
val toks = text_src |
|
17932 | 243 |
|> Symbol.source false |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
244 |
|> T.source NONE (K lexs) pos |
17932 | 245 |
|> Source.exhausted; |
246 |
val trs = toks |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
247 |
|> toplevel_source false NONE (K parser) |
17932 | 248 |
|> Source.exhaust; |
23866
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset
|
249 |
|
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset
|
250 |
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); |
25685 | 251 |
val _ = cond_timeit time "" (fn () => |
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26990
diff
changeset
|
252 |
ThyOutput.process_thy (#1 lexs) OuterKeyword.command_tags is_markup trs toks |
23866
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset
|
253 |
|> Buffer.content |
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset
|
254 |
|> Present.theory_output name); |
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset
|
255 |
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); |
24065 | 256 |
in () end; |
23866
5295671034f8
moved deps_thy to ThyLoad (independent of outer syntax);
wenzelm
parents:
23796
diff
changeset
|
257 |
|
5829 | 258 |
end; |
259 |