Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
1 (* Title: Pure/Isar/outer_syntax.ML
2 Author: Markus Wenzel, TU Muenchen
4 The global Isabelle/Isar outer syntax.
6 Note: the syntax for files is statically determined at the very
7 beginning; for interactive processing it may change dynamically.
10 signature OUTER_SYNTAX =
13 val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
14 val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
15 val check_syntax: unit -> unit
16 type command_spec = (string * Keyword.T) * Position.T
17 val command: command_spec -> string ->
18 (Toplevel.transition -> Toplevel.transition) parser -> unit
19 val markup_command: Thy_Output.markup -> command_spec -> string ->
20 (Toplevel.transition -> Toplevel.transition) parser -> unit
21 val improper_command: command_spec -> string ->
22 (Toplevel.transition -> Toplevel.transition) parser -> unit
23 val local_theory': command_spec -> string ->
24 (bool -> local_theory -> local_theory) parser -> unit
25 val local_theory: command_spec -> string ->
26 (local_theory -> local_theory) parser -> unit
27 val local_theory_to_proof': command_spec -> string ->
28 (bool -> local_theory -> Proof.state) parser -> unit
29 val local_theory_to_proof: command_spec -> string ->
30 (local_theory -> Proof.state) parser -> unit
31 val print_outer_syntax: unit -> unit
32 val scan: Position.T -> string -> Token.T list
33 val parse: Position.T -> string -> Toplevel.transition list
35 val isar: TextIO.instream -> bool -> isar
36 val span_cmts: Token.T list -> Token.T list
37 val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
38 val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
39 (Toplevel.transition * Toplevel.transition list) list
42 structure Outer_Syntax: OUTER_SYNTAX =
49 datatype command = Command of
51 markup: Thy_Output.markup option,
53 parse: (Toplevel.transition -> Toplevel.transition) parser,
57 fun new_command comment markup int_only parse pos =
58 Command {comment = comment, markup = markup, int_only = int_only, parse = parse,
59 pos = pos, id = serial ()};
61 fun command_markup def (name, Command {pos, id, ...}) =
62 Markup.properties (Position.entity_properties_of def id pos)
63 (Markup.entity Markup.commandN name);
70 fun terminate false = Scan.succeed ()
72 Parse.group (fn () => "end of input")
73 (Scan.option Parse.sync -- Parse.semicolon >> K ());
75 fun body cmd (name, _) =
77 SOME (Command {int_only, parse, ...}) =>
78 Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
80 Scan.succeed (false, Toplevel.imperative (fn () =>
81 error ("Bad parser for outer syntax command " ^ quote name))));
85 fun parse_command do_terminate cmd =
86 Parse.semicolon >> K NONE ||
87 Parse.sync >> K NONE ||
88 (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
89 >> (fn ((name, pos), (int_only, f)) =>
90 SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
91 Toplevel.interactive int_only |> f));
96 (* type outer_syntax *)
98 datatype outer_syntax = Outer_Syntax of
99 {commands: command Symtab.table,
100 markups: (string * Thy_Output.markup) list};
102 fun make_outer_syntax commands markups =
103 Outer_Syntax {commands = commands, markups = markups};
105 val empty_outer_syntax = make_outer_syntax Symtab.empty [];
108 fun map_commands f (Outer_Syntax {commands, ...}) =
110 val commands' = f commands;
112 Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
114 in make_outer_syntax commands' markups' end;
116 fun dest_commands (Outer_Syntax {commands, ...}) =
117 commands |> Symtab.dest |> sort_wrt #1
118 |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
120 fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands;
122 fun is_markup (Outer_Syntax {markups, ...}) kind name =
123 AList.lookup (op =) markups name = SOME kind;
127 (** global outer syntax **)
129 type command_spec = (string * Keyword.T) * Position.T;
133 (*synchronized wrt. Keywords*)
134 val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
136 fun add_command (name, kind) cmd = CRITICAL (fn () =>
138 val thy = ML_Context.the_global_context ();
139 val Command {pos, ...} = cmd;
141 (case try (Thy_Header.the_keyword thy) name of
143 if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then ()
144 else error ("Inconsistent outer syntax keyword declaration " ^
145 quote name ^ Position.here pos)
147 if Context.theory_name thy = Context.PureN
148 then Keyword.define (name, SOME kind)
149 else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos));
150 val _ = Position.report pos (command_markup true (name, cmd));
152 Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
153 (if not (Symtab.defined commands name) then ()
154 else warning ("Redefining outer syntax command " ^ quote name);
155 Symtab.update (name, cmd) commands)))
160 fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax));
162 fun check_syntax () =
164 val ((_, major), syntax) = CRITICAL (fn () => (Keyword.dest (), ! global_outer_syntax));
166 (case subtract (op =) (map #1 (dest_commands syntax)) major of
168 | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
171 fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
173 fun command (spec, pos) comment parse =
174 add_command spec (new_command comment NONE false parse pos);
176 fun markup_command markup (spec, pos) comment parse =
177 add_command spec (new_command comment (SOME markup) false parse pos);
179 fun improper_command (spec, pos) comment parse =
180 add_command spec (new_command comment NONE true parse pos);
185 (* local_theory commands *)
187 fun local_theory_command do_print trans command_spec comment parse =
188 command command_spec comment (Parse.opt_target -- parse
189 >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
191 val local_theory' = local_theory_command false Toplevel.local_theory';
192 val local_theory = local_theory_command false Toplevel.local_theory;
193 val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
194 val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
199 fun print_outer_syntax () =
201 val ((keywords, _), outer_syntax) =
202 CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
203 fun pretty_cmd (name, comment, _) =
204 Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
205 val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);
207 [Pretty.strs ("syntax keywords:" :: map quote keywords),
208 Pretty.big_list "commands:" (map pretty_cmd cmds),
209 Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
210 |> Pretty.chunks |> Pretty.writeln
215 (** toplevel parsing **)
219 fun toplevel_source term do_recover cmd src =
222 Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
224 (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
227 |> Token.source_proper
228 |> Source.source Token.stopper
229 (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
230 (Option.map recover do_recover)
231 |> Source.map_filter I
232 |> Source.source Token.stopper
233 (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
234 (Option.map recover do_recover)
235 |> Source.map_filter I
239 (* off-line scanning/parsing *)
244 |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
250 |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
251 |> toplevel_source false NONE lookup_commands_dynamic
255 (* interactive source of toplevel transformers *)
258 (Toplevel.transition, (Toplevel.transition option,
259 (Token.T, (Token.T option, (Token.T, (Token.T,
260 (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
261 Source.source) Source.source) Source.source) Source.source)
262 Source.source) Source.source) Source.source) Source.source;
264 fun isar in_stream term : isar =
267 |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
268 |> toplevel_source term (SOME true) lookup_commands_dynamic;
275 fun cmts (t1 :: t2 :: toks) =
276 if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
277 else cmts (t2 :: toks)
282 val span_cmts = filter Token.is_proper #> cmts;
287 (* read toplevel commands -- fail-safe *)
289 fun read_span outer_syntax toks =
291 val commands = lookup_commands outer_syntax;
293 val proper_range = Position.set_range (Command.proper_range toks);
295 (case find_first Token.is_command toks of
296 SOME tok => Token.position_of tok
297 | NONE => proper_range);
299 fun command_reports tok =
300 if Token.is_command tok then
301 let val name = Token.content_of tok in
302 (case commands name of
304 | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
308 val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
309 val _ = Position.reports_text (token_reports @ maps command_reports toks);
311 if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true)
313 (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
315 if Keyword.is_control (Toplevel.name_of tr) then
316 (Toplevel.malformed pos "Illegal control command", true)
318 | [] => (Toplevel.ignored (Position.set_range (Command.range toks)), false)
319 | _ => (Toplevel.malformed proper_range "Exactly one command expected", true))
320 handle ERROR msg => (Toplevel.malformed proper_range msg, true)
323 fun read_element outer_syntax init {head, proof, proper_proof} =
325 val read = read_span outer_syntax o Thy_Syntax.span_content;
326 val (tr, proper_head) = read head |>> Toplevel.modify_init init;
327 val proof_trs = map read proof |> filter #2 |> map #1;
329 if proper_head andalso proper_proof andalso
330 not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
331 else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)