src/Pure/Isar/outer_syntax.ML
author wenzelm
Mon Dec 10 13:52:33 2012 +0100 (2012-12-10 ago)
changeset 50450 358b6020f8b6
parent 50215 97959912840a
child 51225 3fe0d8d55975
permissions -rw-r--r--
generalized notion of active area, where sendback is just one application;
some support for graphview via active area;
     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 help_outer_syntax: string list -> unit
    32   val print_outer_syntax: unit -> unit
    33   val scan: Position.T -> string -> Token.T list
    34   val parse: Position.T -> string -> Toplevel.transition list
    35   type isar
    36   val isar: TextIO.instream -> bool -> isar
    37   val span_cmts: Token.T list -> Token.T list
    38   val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
    39   val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
    40     (Toplevel.transition * Toplevel.transition list) list
    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   pos: Position.T,
    56   id: serial};
    57 
    58 fun new_command comment markup int_only parse pos =
    59   Command {comment = comment, markup = markup, int_only = int_only, parse = parse,
    60     pos = pos, id = serial ()};
    61 
    62 fun command_markup def (name, Command {pos, id, ...}) =
    63   Markup.properties (Position.entity_properties_of def id pos)
    64     (Markup.entity Markup.commandN name);
    65 
    66 fun pretty_command (cmd as (name, Command {comment, ...})) =
    67   Pretty.block
    68     (Pretty.marks_str
    69       ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]},
    70         command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
    71 
    72 
    73 (* parse command *)
    74 
    75 local
    76 
    77 fun terminate false = Scan.succeed ()
    78   | terminate true =
    79       Parse.group (fn () => "end of input")
    80         (Scan.option Parse.sync -- Parse.semicolon >> K ());
    81 
    82 fun body cmd (name, _) =
    83   (case cmd name of
    84     SOME (Command {int_only, parse, ...}) =>
    85       Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
    86   | NONE =>
    87       Scan.succeed (false, Toplevel.imperative (fn () =>
    88         error ("Bad parser for outer syntax command " ^ quote name))));
    89 
    90 in
    91 
    92 fun parse_command do_terminate cmd =
    93   Parse.semicolon >> K NONE ||
    94   Parse.sync >> K NONE ||
    95   (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
    96     >> (fn ((name, pos), (int_only, f)) =>
    97       SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
    98         Toplevel.interactive int_only |> f));
    99 
   100 end;
   101 
   102 
   103 (* type outer_syntax *)
   104 
   105 datatype outer_syntax = Outer_Syntax of
   106  {commands: command Symtab.table,
   107   markups: (string * Thy_Output.markup) list};
   108 
   109 fun make_outer_syntax commands markups =
   110   Outer_Syntax {commands = commands, markups = markups};
   111 
   112 val empty_outer_syntax = make_outer_syntax Symtab.empty [];
   113 
   114 
   115 fun map_commands f (Outer_Syntax {commands, ...}) =
   116   let
   117     val commands' = f commands;
   118     val markups' =
   119       Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
   120         commands' [];
   121   in make_outer_syntax commands' markups' end;
   122 
   123 fun dest_commands (Outer_Syntax {commands, ...}) =
   124   commands |> Symtab.dest |> sort_wrt #1;
   125 
   126 fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands;
   127 
   128 fun is_markup (Outer_Syntax {markups, ...}) kind name =
   129   AList.lookup (op =) markups name = SOME kind;
   130 
   131 
   132 
   133 (** global outer syntax **)
   134 
   135 type command_spec = (string * Keyword.T) * Position.T;
   136 
   137 local
   138 
   139 (*synchronized wrt. Keywords*)
   140 val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
   141 
   142 fun add_command (name, kind) cmd = CRITICAL (fn () =>
   143   let
   144     val thy = ML_Context.the_global_context ();
   145     val Command {pos, ...} = cmd;
   146     val _ =
   147       (case try (Thy_Header.the_keyword thy) name of
   148         SOME spec =>
   149           if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then ()
   150           else error ("Inconsistent outer syntax keyword declaration " ^
   151             quote name ^ Position.here pos)
   152       | NONE =>
   153           if Context.theory_name thy = Context.PureN
   154           then Keyword.define (name, SOME kind)
   155           else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos));
   156     val _ = Position.report pos (command_markup true (name, cmd));
   157   in
   158     Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
   159      (if not (Symtab.defined commands name) then ()
   160       else warning ("Redefining outer syntax command " ^ quote name);
   161       Symtab.update (name, cmd) commands)))
   162   end);
   163 
   164 in
   165 
   166 fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax));
   167 
   168 fun check_syntax () =
   169   let
   170     val ((_, major), syntax) = CRITICAL (fn () => (Keyword.dest (), ! global_outer_syntax));
   171   in
   172     (case subtract (op =) (map #1 (dest_commands syntax)) major of
   173       [] => ()
   174     | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
   175   end;
   176 
   177 fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
   178 
   179 fun command (spec, pos) comment parse =
   180   add_command spec (new_command comment NONE false parse pos);
   181 
   182 fun markup_command markup (spec, pos) comment parse =
   183   add_command spec (new_command comment (SOME markup) false parse pos);
   184 
   185 fun improper_command (spec, pos) comment parse =
   186   add_command spec (new_command comment NONE true parse pos);
   187 
   188 end;
   189 
   190 
   191 (* local_theory commands *)
   192 
   193 fun local_theory_command do_print trans command_spec comment parse =
   194   command command_spec comment (Parse.opt_target -- parse
   195     >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
   196 
   197 val local_theory' = local_theory_command false Toplevel.local_theory';
   198 val local_theory = local_theory_command false Toplevel.local_theory;
   199 val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
   200 val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
   201 
   202 
   203 (* inspect syntax *)
   204 
   205 fun help_outer_syntax pats =
   206   dest_commands (#2 (get_syntax ()))
   207   |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
   208   |> map pretty_command
   209   |> Pretty.chunks |> Pretty.writeln;
   210 
   211 fun print_outer_syntax () =
   212   let
   213     val ((keywords, _), outer_syntax) =
   214       CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
   215     val (int_cmds, cmds) =
   216       List.partition (fn (_, Command {int_only, ...}) => int_only) (dest_commands outer_syntax);
   217   in
   218     [Pretty.strs ("syntax keywords:" :: map quote keywords),
   219       Pretty.big_list "commands:" (map pretty_command cmds),
   220       Pretty.big_list "interactive-only commands:" (map pretty_command int_cmds)]
   221     |> Pretty.chunks |> Pretty.writeln
   222   end;
   223 
   224 
   225 
   226 (** toplevel parsing **)
   227 
   228 (* basic sources *)
   229 
   230 fun toplevel_source term do_recover cmd src =
   231   let
   232     val no_terminator =
   233       Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
   234     fun recover int =
   235       (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
   236   in
   237     src
   238     |> Token.source_proper
   239     |> Source.source Token.stopper
   240       (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
   241         (Option.map recover do_recover)
   242     |> Source.map_filter I
   243     |> Source.source Token.stopper
   244         (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
   245         (Option.map recover do_recover)
   246     |> Source.map_filter I
   247   end;
   248 
   249 
   250 (* off-line scanning/parsing *)
   251 
   252 fun scan pos str =
   253   Source.of_string str
   254   |> Symbol.source
   255   |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   256   |> Source.exhaust;
   257 
   258 fun parse pos str =
   259   Source.of_string str
   260   |> Symbol.source
   261   |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   262   |> toplevel_source false NONE lookup_commands_dynamic
   263   |> Source.exhaust;
   264 
   265 
   266 (* interactive source of toplevel transformers *)
   267 
   268 type isar =
   269   (Toplevel.transition, (Toplevel.transition option,
   270     (Token.T, (Token.T option, (Token.T, (Token.T,
   271       (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
   272   Source.source) Source.source) Source.source) Source.source)
   273   Source.source) Source.source) Source.source) Source.source;
   274 
   275 fun isar in_stream term : isar =
   276   Source.tty in_stream
   277   |> Symbol.source
   278   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   279   |> toplevel_source term (SOME true) lookup_commands_dynamic;
   280 
   281 
   282 (* side-comments *)
   283 
   284 local
   285 
   286 fun cmts (t1 :: t2 :: toks) =
   287       if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
   288       else cmts (t2 :: toks)
   289   | cmts _ = [];
   290 
   291 in
   292 
   293 val span_cmts = filter Token.is_proper #> cmts;
   294 
   295 end;
   296 
   297 
   298 (* read toplevel commands -- fail-safe *)
   299 
   300 fun read_span outer_syntax toks =
   301   let
   302     val commands = lookup_commands outer_syntax;
   303 
   304     val proper_range = Position.set_range (Command.proper_range toks);
   305     val pos =
   306       (case find_first Token.is_command toks of
   307         SOME tok => Token.position_of tok
   308       | NONE => proper_range);
   309 
   310     fun command_reports tok =
   311       if Token.is_command tok then
   312         let val name = Token.content_of tok in
   313           (case commands name of
   314             NONE => []
   315           | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")])
   316         end
   317       else [];
   318 
   319     val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
   320     val _ = Position.reports_text (token_reports @ maps command_reports toks);
   321   in
   322     if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true)
   323     else
   324       (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
   325         [tr] =>
   326           if Keyword.is_control (Toplevel.name_of tr) then
   327             (Toplevel.malformed pos "Illegal control command", true)
   328           else (tr, true)
   329       | [] => (Toplevel.ignored (Position.set_range (Command.range toks)), false)
   330       | _ => (Toplevel.malformed proper_range "Exactly one command expected", true))
   331       handle ERROR msg => (Toplevel.malformed proper_range msg, true)
   332   end;
   333 
   334 fun read_element outer_syntax init {head, proof, proper_proof} =
   335   let
   336     val read = read_span outer_syntax o Thy_Syntax.span_content;
   337     val (tr, proper_head) = read head |>> Toplevel.modify_init init;
   338     val proof_trs = map read proof |> filter #2 |> map #1;
   339   in
   340     if proper_head andalso proper_proof andalso
   341       not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
   342     else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
   343   end;
   344 
   345 end;
   346