src/Pure/Isar/outer_syntax.ML
author wenzelm
Mon May 14 22:22:47 2018 +0200 (13 months ago)
changeset 68184 6c693b2700b3
parent 67499 bbb86f719d4b
child 68729 3a02b424d5fb
permissions -rw-r--r--
support for dynamic document output while editing;
     1 (*  Title:      Pure/Isar/outer_syntax.ML
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 Isabelle/Isar outer syntax.
     5 *)
     6 
     7 signature OUTER_SYNTAX =
     8 sig
     9   val help: theory -> string list -> unit
    10   val print_commands: theory -> unit
    11   type command_keyword = string * Position.T
    12   val command: command_keyword -> string ->
    13     (Toplevel.transition -> Toplevel.transition) parser -> unit
    14   val maybe_begin_local_theory: command_keyword -> string ->
    15     (local_theory -> local_theory) parser -> (theory -> local_theory) parser -> unit
    16   val local_theory': command_keyword -> string ->
    17     (bool -> local_theory -> local_theory) parser -> unit
    18   val local_theory: command_keyword -> string ->
    19     (local_theory -> local_theory) parser -> unit
    20   val local_theory_to_proof': command_keyword -> string ->
    21     (bool -> local_theory -> Proof.state) parser -> unit
    22   val local_theory_to_proof: command_keyword -> string ->
    23     (local_theory -> Proof.state) parser -> unit
    24   val bootstrap: bool Config.T
    25   val parse_tokens: theory -> Token.T list -> Toplevel.transition list
    26   val parse: theory -> Position.T -> string -> Toplevel.transition list
    27   val parse_spans: Token.T list -> Command_Span.span list
    28   val make_span: Token.T list -> Command_Span.span
    29   val command_reports: theory -> Token.T -> Position.report_text list
    30   val check_command: Proof.context -> command_keyword -> string
    31 end;
    32 
    33 structure Outer_Syntax: OUTER_SYNTAX =
    34 struct
    35 
    36 (** outer syntax **)
    37 
    38 (* errors *)
    39 
    40 fun err_command msg name ps =
    41   error (msg ^ quote (Markup.markup Markup.keyword1 name) ^ Position.here_list ps);
    42 
    43 fun err_dup_command name ps =
    44   err_command "Duplicate outer syntax command " name ps;
    45 
    46 
    47 (* command parsers *)
    48 
    49 datatype command_parser =
    50   Parser of (Toplevel.transition -> Toplevel.transition) parser |
    51   Restricted_Parser of
    52     (bool * Position.T) option -> (Toplevel.transition -> Toplevel.transition) parser;
    53 
    54 datatype command = Command of
    55  {comment: string,
    56   command_parser: command_parser,
    57   pos: Position.T,
    58   id: serial};
    59 
    60 fun eq_command (Command {id = id1, ...}, Command {id = id2, ...}) = id1 = id2;
    61 
    62 fun new_command comment command_parser pos =
    63   Command {comment = comment, command_parser = command_parser, pos = pos, id = serial ()};
    64 
    65 fun command_pos (Command {pos, ...}) = pos;
    66 
    67 fun command_markup def (name, Command {pos, id, ...}) =
    68   Markup.properties (Position.entity_properties_of def id pos)
    69     (Markup.entity Markup.commandN name);
    70 
    71 fun pretty_command (cmd as (name, Command {comment, ...})) =
    72   Pretty.block
    73     (Pretty.marks_str
    74       ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]},
    75         command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
    76 
    77 
    78 (* theory data *)
    79 
    80 structure Data = Theory_Data
    81 (
    82   type T = command Symtab.table;
    83   val empty = Symtab.empty;
    84   val extend = I;
    85   fun merge data : T =
    86     data |> Symtab.join (fn name => fn (cmd1, cmd2) =>
    87       if eq_command (cmd1, cmd2) then raise Symtab.SAME
    88       else err_dup_command name [command_pos cmd1, command_pos cmd2]);
    89 );
    90 
    91 val get_commands = Data.get;
    92 val dest_commands = get_commands #> Symtab.dest #> sort_by #1;
    93 val lookup_commands = Symtab.lookup o get_commands;
    94 
    95 fun help thy pats =
    96   dest_commands thy
    97   |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
    98   |> map pretty_command
    99   |> Pretty.writeln_chunks;
   100 
   101 fun print_commands thy =
   102   let
   103     val keywords = Thy_Header.get_keywords thy;
   104     val minor = Scan.dest_lexicon (Keyword.minor_keywords keywords);
   105     val commands = dest_commands thy;
   106   in
   107     [Pretty.strs ("keywords:" :: map quote minor),
   108       Pretty.big_list "commands:" (map pretty_command commands)]
   109     |> Pretty.writeln_chunks
   110   end;
   111 
   112 
   113 (* maintain commands *)
   114 
   115 fun add_command name cmd thy =
   116   if member (op =) Thy_Header.bootstrap_thys (Context.theory_name thy) then thy
   117   else
   118     let
   119       val _ =
   120         Keyword.is_command (Thy_Header.get_keywords thy) name orelse
   121           err_command "Undeclared outer syntax command " name [command_pos cmd];
   122       val _ =
   123         (case lookup_commands thy name of
   124           NONE => ()
   125         | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
   126       val _ =
   127         Context_Position.report_generic (Context.the_generic_context ())
   128           (command_pos cmd) (command_markup true (name, cmd));
   129     in Data.map (Symtab.update (name, cmd)) thy end;
   130 
   131 val _ = Theory.setup (Theory.at_end (fn thy =>
   132   let
   133     val command_keywords =
   134       Scan.dest_lexicon (Keyword.major_keywords (Thy_Header.get_keywords thy));
   135     val _ =
   136       (case subtract (op =) (map #1 (dest_commands thy)) command_keywords of
   137         [] => ()
   138       | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
   139   in NONE end));
   140 
   141 
   142 (* implicit theory setup *)
   143 
   144 type command_keyword = string * Position.T;
   145 
   146 fun raw_command (name, pos) comment command_parser =
   147   let val setup = add_command name (new_command comment command_parser pos)
   148   in Context.>> (Context.mapping setup (Local_Theory.background_theory setup)) end;
   149 
   150 fun command (name, pos) comment parse =
   151   raw_command (name, pos) comment (Parser parse);
   152 
   153 fun maybe_begin_local_theory command_keyword comment parse_local parse_global =
   154   raw_command command_keyword comment
   155     (Restricted_Parser (fn restricted =>
   156       Parse.opt_target -- parse_local
   157         >> (fn (target, f) => Toplevel.local_theory restricted target f) ||
   158       (if is_some restricted then Scan.fail
   159        else parse_global >> Toplevel.begin_local_theory true)));
   160 
   161 fun local_theory_command trans command_keyword comment parse =
   162   raw_command command_keyword comment
   163     (Restricted_Parser (fn restricted =>
   164       Parse.opt_target -- parse >> (fn (target, f) => trans restricted target f)));
   165 
   166 val local_theory' = local_theory_command Toplevel.local_theory';
   167 val local_theory = local_theory_command Toplevel.local_theory;
   168 val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof';
   169 val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;
   170 
   171 
   172 
   173 (** toplevel parsing **)
   174 
   175 (* parse commands *)
   176 
   177 val bootstrap =
   178   Config.bool (Config.declare ("Outer_Syntax.bootstrap", \<^here>) (K (Config.Bool true)));
   179 
   180 local
   181 
   182 val before_command =
   183   Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
   184 
   185 fun parse_command thy =
   186   Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
   187     let
   188       val keywords = Thy_Header.get_keywords thy;
   189       val command_tags = Parse.command -- Parse.tags;
   190       val tr0 =
   191         Toplevel.empty
   192         |> Toplevel.name name
   193         |> Toplevel.position pos
   194         |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
   195         |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
   196     in
   197       (case lookup_commands thy name of
   198         SOME (Command {command_parser = Parser parse, ...}) =>
   199           Parse.!!! (command_tags |-- parse) >> (fn f => f tr0)
   200       | SOME (Command {command_parser = Restricted_Parser parse, ...}) =>
   201           before_command :|-- (fn restricted =>
   202             Parse.!!! (command_tags |-- parse restricted)) >> (fn f => f tr0)
   203       | NONE =>
   204           Scan.fail_with (fn _ => fn _ =>
   205             let
   206               val msg =
   207                 if Config.get_global thy bootstrap
   208                 then "missing theory context for command "
   209                 else "undefined command ";
   210             in msg ^ quote (Markup.markup Markup.keyword1 name) end))
   211     end);
   212 
   213 in
   214 
   215 fun parse_tokens thy =
   216   filter Token.is_proper
   217   #> Source.of_list
   218   #> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs))
   219   #> Source.exhaust;
   220 
   221 fun parse thy pos text =
   222   Symbol_Pos.explode (text, pos)
   223   |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false}
   224   |> parse_tokens thy;
   225 
   226 end;
   227 
   228 
   229 (* parse spans *)
   230 
   231 local
   232 
   233 fun ship span =
   234   let
   235     val kind =
   236       if forall Token.is_improper span then Command_Span.Ignored_Span
   237       else if exists Token.is_error span then Command_Span.Malformed_Span
   238       else
   239         (case find_first Token.is_command span of
   240           NONE => Command_Span.Malformed_Span
   241         | SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd));
   242   in cons (Command_Span.Span (kind, span)) end;
   243 
   244 fun flush (result, content, improper) =
   245   result
   246   |> not (null content) ? ship (rev content)
   247   |> not (null improper) ? ship (rev improper);
   248 
   249 fun parse tok (result, content, improper) =
   250   if Token.is_improper tok then (result, content, tok :: improper)
   251   else if Token.is_command_modifier tok orelse
   252     Token.is_command tok andalso
   253       (not (exists Token.is_command_modifier content) orelse exists Token.is_command content)
   254   then (flush (result, content, improper), [tok], [])
   255   else (result, tok :: (improper @ content), []);
   256 
   257 in
   258 
   259 fun parse_spans toks =
   260   fold parse toks ([], [], []) |> flush |> rev;
   261 
   262 end;
   263 
   264 fun make_span toks =
   265   (case parse_spans toks of
   266     [span] => span
   267   | _ => Command_Span.Span (Command_Span.Malformed_Span, toks));
   268 
   269 
   270 (* check commands *)
   271 
   272 fun command_reports thy tok =
   273   if Token.is_command tok then
   274     let val name = Token.content_of tok in
   275       (case lookup_commands thy name of
   276         NONE => []
   277       | SOME cmd => [((Token.pos_of tok, command_markup false (name, cmd)), "")])
   278     end
   279   else [];
   280 
   281 fun check_command ctxt (name, pos) =
   282   let
   283     val thy = Proof_Context.theory_of ctxt;
   284     val keywords = Thy_Header.get_keywords thy;
   285   in
   286     if Keyword.is_command keywords name then
   287       let
   288         val markup =
   289           Token.explode0 keywords name
   290           |> maps (command_reports thy)
   291           |> map (#2 o #1);
   292         val _ = Context_Position.reports ctxt (map (pair pos) markup);
   293       in name end
   294     else
   295       let
   296         val completion =
   297           Completion.make (name, pos)
   298             (fn completed =>
   299               Keyword.dest_commands keywords
   300               |> filter completed
   301               |> sort_strings
   302               |> map (fn a => (a, (Markup.commandN, a))));
   303         val report = Markup.markup_report (Completion.reported_text completion);
   304       in error ("Bad command " ^ quote name ^ Position.here pos ^ report) end
   305   end;
   306 
   307 
   308 (* 'ML' command -- required for bootstrapping Isar *)
   309 
   310 val _ =
   311   command ("ML", \<^here>) "ML text within theory or local theory"
   312     (Parse.ML_source >> (fn source =>
   313       Toplevel.generic_theory
   314         (ML_Context.exec (fn () =>
   315             ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
   316           Local_Theory.propagate_ml_env)));
   317 
   318 end;