src/Pure/Isar/outer_syntax.ML
author wenzelm
Sun Aug 21 20:42:26 2011 +0200 (2011-08-21)
changeset 44357 5f5649ac8235
parent 44187 88d770052bac
child 44478 4fdb1009a370
permissions -rw-r--r--
tuned Parse.group: delayed failure message;
     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 command: string -> string -> Keyword.T ->
    16     (Toplevel.transition -> Toplevel.transition) parser -> unit
    17   val markup_command: Thy_Output.markup -> string -> string -> Keyword.T ->
    18     (Toplevel.transition -> Toplevel.transition) parser -> unit
    19   val improper_command: string -> string -> Keyword.T ->
    20     (Toplevel.transition -> Toplevel.transition) parser -> unit
    21   val internal_command: string ->
    22     (Toplevel.transition -> Toplevel.transition) parser -> unit
    23   val local_theory': string -> string -> Keyword.T ->
    24     (bool -> local_theory -> local_theory) parser -> unit
    25   val local_theory: string -> string -> Keyword.T ->
    26     (local_theory -> local_theory) parser -> unit
    27   val local_theory_to_proof': string -> string -> Keyword.T ->
    28     (bool -> local_theory -> Proof.state) parser -> unit
    29   val local_theory_to_proof: string -> string -> Keyword.T ->
    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   val process_file: Path.T -> theory -> theory
    35   type isar
    36   val isar: TextIO.instream -> bool -> isar
    37   val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
    38   val prepare_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
    39     (Toplevel.transition * Toplevel.transition list) list
    40   val prepare_command: Position.T -> string -> Toplevel.transition
    41 end;
    42 
    43 structure Outer_Syntax: OUTER_SYNTAX =
    44 struct
    45 
    46 (** outer syntax **)
    47 
    48 (* command parsers *)
    49 
    50 datatype command = Command of
    51  {comment: string,
    52   markup: Thy_Output.markup option,
    53   int_only: bool,
    54   parse: (Toplevel.transition -> Toplevel.transition) parser};
    55 
    56 fun make_command comment markup int_only parse =
    57   Command {comment = comment, markup = markup, int_only = int_only, parse = parse};
    58 
    59 
    60 (* parse command *)
    61 
    62 local
    63 
    64 fun terminate false = Scan.succeed ()
    65   | terminate true =
    66       Parse.group (fn () => "end of input")
    67         (Scan.option Parse.sync -- Parse.semicolon >> K ());
    68 
    69 fun body cmd (name, _) =
    70   (case cmd name of
    71     SOME (Command {int_only, parse, ...}) =>
    72       Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
    73   | NONE => raise Fail ("No parser for outer syntax command " ^ quote name));
    74 
    75 in
    76 
    77 fun parse_command do_terminate cmd =
    78   Parse.semicolon >> K NONE ||
    79   Parse.sync >> K NONE ||
    80   (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
    81     >> (fn ((name, pos), (int_only, f)) =>
    82       SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
    83         Toplevel.interactive int_only |> f));
    84 
    85 end;
    86 
    87 
    88 (* type outer_syntax *)
    89 
    90 datatype outer_syntax = Outer_Syntax of
    91  {commands: command Symtab.table,
    92   markups: (string * Thy_Output.markup) list};
    93 
    94 fun make_outer_syntax commands markups =
    95   Outer_Syntax {commands = commands, markups = markups};
    96 
    97 val empty_outer_syntax = make_outer_syntax Symtab.empty [];
    98 
    99 
   100 fun map_commands f (Outer_Syntax {commands, ...}) =
   101   let
   102     val commands' = f commands;
   103     val markups' =
   104       Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
   105         commands' [];
   106   in make_outer_syntax commands' markups' end;
   107 
   108 fun dest_commands (Outer_Syntax {commands, ...}) =
   109   commands |> Symtab.dest |> sort_wrt #1
   110   |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
   111 
   112 fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands;
   113 
   114 fun is_markup (Outer_Syntax {markups, ...}) kind name =
   115   AList.lookup (op =) markups name = SOME kind;
   116 
   117 
   118 
   119 (** global outer syntax **)
   120 
   121 local
   122 
   123 (*synchronized wrt. Keywords*)
   124 val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
   125 
   126 fun add_command name kind cmd = CRITICAL (fn () =>
   127  (Keyword.command name kind;
   128   Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
   129    (if not (Symtab.defined commands name) then ()
   130     else warning ("Redefining outer syntax command " ^ quote name);
   131     Symtab.update (name, cmd) commands)))));
   132 
   133 in
   134 
   135 fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax));
   136 
   137 fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
   138 
   139 fun command name comment kind parse =
   140   add_command name kind (make_command comment NONE false parse);
   141 
   142 fun markup_command markup name comment kind parse =
   143   add_command name kind (make_command comment (SOME markup) false parse);
   144 
   145 fun improper_command name comment kind parse =
   146   add_command name kind (make_command comment NONE true parse);
   147 
   148 fun internal_command name parse =
   149   command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
   150 
   151 end;
   152 
   153 
   154 (* local_theory commands *)
   155 
   156 fun local_theory_command do_print trans name comment kind parse =
   157   command name comment kind (Parse.opt_target -- parse
   158     >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
   159 
   160 val local_theory' = local_theory_command false Toplevel.local_theory';
   161 val local_theory = local_theory_command false Toplevel.local_theory;
   162 val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
   163 val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
   164 
   165 
   166 (* inspect syntax *)
   167 
   168 fun print_outer_syntax () =
   169   let
   170     val (keywords, outer_syntax) =
   171       CRITICAL (fn () => (Keyword.dest_keywords (), #2 (get_syntax ())));
   172     fun pretty_cmd (name, comment, _) =
   173       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   174     val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);
   175   in
   176     [Pretty.strs ("syntax keywords:" :: map quote keywords),
   177       Pretty.big_list "commands:" (map pretty_cmd cmds),
   178       Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
   179     |> Pretty.chunks |> Pretty.writeln
   180   end;
   181 
   182 
   183 
   184 (** toplevel parsing **)
   185 
   186 (* basic sources *)
   187 
   188 fun toplevel_source term do_recover cmd src =
   189   let
   190     val no_terminator =
   191       Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
   192     fun recover int =
   193       (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
   194   in
   195     src
   196     |> Token.source_proper
   197     |> Source.source Token.stopper
   198       (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
   199         (Option.map recover do_recover)
   200     |> Source.map_filter I
   201     |> Source.source Token.stopper
   202         (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
   203         (Option.map recover do_recover)
   204     |> Source.map_filter I
   205   end;
   206 
   207 
   208 (* off-line scanning/parsing *)
   209 
   210 fun scan pos str =
   211   Source.of_string str
   212   |> Symbol.source
   213   |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   214   |> Source.exhaust;
   215 
   216 fun parse pos str =
   217   Source.of_string str
   218   |> Symbol.source
   219   |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   220   |> toplevel_source false NONE lookup_commands_dynamic
   221   |> Source.exhaust;
   222 
   223 
   224 (* process file *)
   225 
   226 fun process_file path thy =
   227   let
   228     val trs = parse (Path.position path) (File.read path);
   229     val init = Toplevel.init_theory (K thy) Toplevel.empty;
   230     val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
   231   in
   232     (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
   233       (true, Context.Theory thy') => thy'
   234     | _ => error "Bad result state: global theory expected")
   235   end;
   236 
   237 
   238 (* interactive source of toplevel transformers *)
   239 
   240 type isar =
   241   (Toplevel.transition, (Toplevel.transition option,
   242     (Token.T, (Token.T option, (Token.T, (Token.T,
   243       (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
   244   Source.source) Source.source) Source.source) Source.source)
   245   Source.source) Source.source) Source.source) Source.source;
   246 
   247 fun isar in_stream term : isar =
   248   Source.tty in_stream
   249   |> Symbol.source
   250   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   251   |> toplevel_source term (SOME true) lookup_commands_dynamic;
   252 
   253 
   254 (* prepare toplevel commands -- fail-safe *)
   255 
   256 val not_singleton = "Exactly one command expected";
   257 
   258 fun prepare_span outer_syntax span =
   259   let
   260     val commands = lookup_commands outer_syntax;
   261     val range_pos = Position.set_range (Thy_Syntax.span_range span);
   262     val toks = Thy_Syntax.span_content span;
   263     val _ = List.app Thy_Syntax.report_token toks;
   264   in
   265     (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
   266       [tr] =>
   267         if Keyword.is_control (Toplevel.name_of tr) then
   268           (Toplevel.malformed range_pos "Illegal control command", true)
   269         else (tr, true)
   270     | [] => (Toplevel.ignored range_pos, false)
   271     | _ => (Toplevel.malformed range_pos not_singleton, true))
   272     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   273   end;
   274 
   275 fun prepare_element outer_syntax init {head, proof, proper_proof} =
   276   let
   277     val (tr, proper_head) = prepare_span outer_syntax head |>> Toplevel.modify_init init;
   278     val proof_trs = map (prepare_span outer_syntax) proof |> filter #2 |> map #1;
   279   in
   280     if proper_head andalso proper_proof then [(tr, proof_trs)]
   281     else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
   282   end;
   283 
   284 fun prepare_command pos str =
   285   let val (lexs, outer_syntax) = get_syntax () in
   286     (case Thy_Syntax.parse_spans lexs pos str of
   287       [span] => #1 (prepare_span outer_syntax span)
   288     | _ => Toplevel.malformed pos not_singleton)
   289   end;
   290 
   291 end;
   292