src/Pure/Isar/outer_syntax.ML
author wenzelm
Sat Aug 11 17:24:21 2012 +0200 (2012-08-11 ago)
changeset 48768 abc45de5bb22
parent 48749 c197b3c3e7fa
child 48771 2ea997196d04
permissions -rw-r--r--
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
     1 (*  Title:      Pure/Isar/outer_syntax.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 The global Isabelle/Isar outer syntax.
     5 
     6 Note: the syntax for files is statically determined at the very
     7 beginning; for interactive processing it may change dynamically.
     8 *)
     9 
    10 signature OUTER_SYNTAX =
    11 sig
    12   type 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
    34   type isar
    35   val isar: TextIO.instream -> bool -> isar
    36   val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
    37   val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
    38     (Toplevel.transition * Toplevel.transition list) list
    39 end;
    40 
    41 structure Outer_Syntax: OUTER_SYNTAX =
    42 struct
    43 
    44 (** outer syntax **)
    45 
    46 (* command parsers *)
    47 
    48 datatype command = Command of
    49  {comment: string,
    50   markup: Thy_Output.markup option,
    51   int_only: bool,
    52   parse: (Toplevel.transition -> Toplevel.transition) parser,
    53   pos: Position.T,
    54   id: serial};
    55 
    56 fun new_command comment markup int_only parse pos =
    57   Command {comment = comment, markup = markup, int_only = int_only, parse = parse,
    58     pos = pos, id = serial ()};
    59 
    60 fun command_markup def (name, Command {pos, id, ...}) =
    61   Markup.properties (Position.entity_properties_of def id pos)
    62     (Isabelle_Markup.entity Isabelle_Markup.commandN name);
    63 
    64 
    65 (* parse command *)
    66 
    67 local
    68 
    69 fun terminate false = Scan.succeed ()
    70   | terminate true =
    71       Parse.group (fn () => "end of input")
    72         (Scan.option Parse.sync -- Parse.semicolon >> K ());
    73 
    74 fun body cmd (name, _) =
    75   (case cmd name of
    76     SOME (Command {int_only, parse, ...}) =>
    77       Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
    78   | NONE =>
    79       Scan.succeed (false, Toplevel.imperative (fn () =>
    80         error ("Bad parser for outer syntax command " ^ quote name))));
    81 
    82 in
    83 
    84 fun parse_command do_terminate cmd =
    85   Parse.semicolon >> K NONE ||
    86   Parse.sync >> K NONE ||
    87   (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
    88     >> (fn ((name, pos), (int_only, f)) =>
    89       SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
    90         Toplevel.interactive int_only |> f));
    91 
    92 end;
    93 
    94 
    95 (* type outer_syntax *)
    96 
    97 datatype outer_syntax = Outer_Syntax of
    98  {commands: command Symtab.table,
    99   markups: (string * Thy_Output.markup) list};
   100 
   101 fun make_outer_syntax commands markups =
   102   Outer_Syntax {commands = commands, markups = markups};
   103 
   104 val empty_outer_syntax = make_outer_syntax Symtab.empty [];
   105 
   106 
   107 fun map_commands f (Outer_Syntax {commands, ...}) =
   108   let
   109     val commands' = f commands;
   110     val markups' =
   111       Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
   112         commands' [];
   113   in make_outer_syntax commands' markups' end;
   114 
   115 fun dest_commands (Outer_Syntax {commands, ...}) =
   116   commands |> Symtab.dest |> sort_wrt #1
   117   |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
   118 
   119 fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands;
   120 
   121 fun is_markup (Outer_Syntax {markups, ...}) kind name =
   122   AList.lookup (op =) markups name = SOME kind;
   123 
   124 
   125 
   126 (** global outer syntax **)
   127 
   128 type command_spec = (string * Keyword.T) * Position.T;
   129 
   130 local
   131 
   132 (*synchronized wrt. Keywords*)
   133 val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
   134 
   135 fun add_command (name, kind) cmd = CRITICAL (fn () =>
   136   let
   137     val thy = ML_Context.the_global_context ();
   138     val Command {pos, ...} = cmd;
   139     val _ =
   140       (case try (Thy_Header.the_keyword thy) name of
   141         SOME spec =>
   142           if Option.map #1 spec = SOME (Keyword.kind_of kind) then ()
   143           else error ("Inconsistent outer syntax keyword declaration " ^
   144             quote name ^ Position.str_of pos)
   145       | NONE =>
   146           if Context.theory_name thy = Context.PureN
   147           then Keyword.define (name, SOME kind)
   148           else error ("Undeclared outer syntax command " ^ quote name ^ Position.str_of pos));
   149     val _ = Position.report pos (command_markup true (name, cmd));
   150   in
   151     Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
   152      (if not (Symtab.defined commands name) then ()
   153       else warning ("Redefining outer syntax command " ^ quote name);
   154       Symtab.update (name, cmd) commands)))
   155   end);
   156 
   157 in
   158 
   159 fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax));
   160 
   161 fun check_syntax () =
   162   let
   163     val ((_, major), syntax) = CRITICAL (fn () => (Keyword.dest (), ! global_outer_syntax));
   164   in
   165     (case subtract (op =) (map #1 (dest_commands syntax)) major of
   166       [] => ()
   167     | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
   168   end;
   169 
   170 fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
   171 
   172 fun command (spec, pos) comment parse =
   173   add_command spec (new_command comment NONE false parse pos);
   174 
   175 fun markup_command markup (spec, pos) comment parse =
   176   add_command spec (new_command comment (SOME markup) false parse pos);
   177 
   178 fun improper_command (spec, pos) comment parse =
   179   add_command spec (new_command comment NONE true parse pos);
   180 
   181 end;
   182 
   183 
   184 (* local_theory commands *)
   185 
   186 fun local_theory_command do_print trans command_spec comment parse =
   187   command command_spec comment (Parse.opt_target -- parse
   188     >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
   189 
   190 val local_theory' = local_theory_command false Toplevel.local_theory';
   191 val local_theory = local_theory_command false Toplevel.local_theory;
   192 val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
   193 val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
   194 
   195 
   196 (* inspect syntax *)
   197 
   198 fun print_outer_syntax () =
   199   let
   200     val ((keywords, _), outer_syntax) =
   201       CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
   202     fun pretty_cmd (name, comment, _) =
   203       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   204     val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);
   205   in
   206     [Pretty.strs ("syntax keywords:" :: map quote keywords),
   207       Pretty.big_list "commands:" (map pretty_cmd cmds),
   208       Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
   209     |> Pretty.chunks |> Pretty.writeln
   210   end;
   211 
   212 
   213 
   214 (** toplevel parsing **)
   215 
   216 (* basic sources *)
   217 
   218 fun toplevel_source term do_recover cmd src =
   219   let
   220     val no_terminator =
   221       Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
   222     fun recover int =
   223       (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
   224   in
   225     src
   226     |> Token.source_proper
   227     |> Source.source Token.stopper
   228       (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
   229         (Option.map recover do_recover)
   230     |> Source.map_filter I
   231     |> Source.source Token.stopper
   232         (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
   233         (Option.map recover do_recover)
   234     |> Source.map_filter I
   235   end;
   236 
   237 
   238 (* off-line scanning/parsing *)
   239 
   240 fun scan pos str =
   241   Source.of_string str
   242   |> Symbol.source
   243   |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   244   |> Source.exhaust;
   245 
   246 fun parse pos str =
   247   Source.of_string str
   248   |> Symbol.source
   249   |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   250   |> toplevel_source false NONE lookup_commands_dynamic
   251   |> Source.exhaust;
   252 
   253 
   254 (* interactive source of toplevel transformers *)
   255 
   256 type isar =
   257   (Toplevel.transition, (Toplevel.transition option,
   258     (Token.T, (Token.T option, (Token.T, (Token.T,
   259       (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
   260   Source.source) Source.source) Source.source) Source.source)
   261   Source.source) Source.source) Source.source) Source.source;
   262 
   263 fun isar in_stream term : isar =
   264   Source.tty in_stream
   265   |> Symbol.source
   266   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   267   |> toplevel_source term (SOME true) lookup_commands_dynamic;
   268 
   269 
   270 (* read toplevel commands -- fail-safe *)
   271 
   272 fun read_span outer_syntax toks =
   273   let
   274     val commands = lookup_commands outer_syntax;
   275 
   276     val range_pos = Position.set_range (Token.range toks);
   277     val pos =
   278       (case find_first Token.is_command toks of
   279         SOME tok => Token.position_of tok
   280       | NONE => range_pos);
   281 
   282     fun command_reports tok =
   283       if Token.is_command tok then
   284         let val name = Token.content_of tok in
   285           (case commands name of
   286             NONE => []
   287           | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
   288         end
   289       else [];
   290 
   291     val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
   292     val _ = Position.reports_text (token_reports @ maps command_reports toks);
   293   in
   294     if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true)
   295     else
   296       (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
   297         [tr] =>
   298           if Keyword.is_control (Toplevel.name_of tr) then
   299             (Toplevel.malformed pos "Illegal control command", true)
   300           else (tr, true)
   301       | [] => (Toplevel.ignored range_pos, false)
   302       | _ => (Toplevel.malformed range_pos "Exactly one command expected", true))
   303       handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   304   end;
   305 
   306 fun read_element outer_syntax init {head, proof, proper_proof} =
   307   let
   308     val read = read_span outer_syntax o Thy_Syntax.span_content;
   309     val (tr, proper_head) = read head |>> Toplevel.modify_init init;
   310     val proof_trs = map read proof |> filter #2 |> map #1;
   311   in
   312     if proper_head andalso proper_proof andalso
   313       not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
   314     else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
   315   end;
   316 
   317 end;
   318