src/Pure/Isar/outer_syntax.ML
author wenzelm
Sun May 30 21:34:19 2010 +0200 (2010-05-30)
changeset 37198 3af985b10550
parent 36959 f5417836dbea
child 37216 3165bc303f66
permissions -rw-r--r--
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information;
fall back on ML_Context.eval_text if there is no position or no surrounding text;
proper Args.name_source_position for method "tactic" and "raw_tactic";
tuned;
     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   val command: string -> string -> Keyword.T ->
    13     (Toplevel.transition -> Toplevel.transition) parser -> unit
    14   val markup_command: ThyOutput.markup -> string -> string -> Keyword.T ->
    15     (Toplevel.transition -> Toplevel.transition) parser -> unit
    16   val improper_command: string -> string -> Keyword.T ->
    17     (Toplevel.transition -> Toplevel.transition) parser -> unit
    18   val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
    19   val local_theory': string -> string -> Keyword.T ->
    20     (bool -> local_theory -> local_theory) parser -> unit
    21   val local_theory: string -> string -> Keyword.T ->
    22     (local_theory -> local_theory) parser -> unit
    23   val local_theory_to_proof': string -> string -> Keyword.T ->
    24     (bool -> local_theory -> Proof.state) parser -> unit
    25   val local_theory_to_proof: string -> string -> Keyword.T ->
    26     (local_theory -> Proof.state) parser -> unit
    27   val print_outer_syntax: unit -> unit
    28   val scan: Position.T -> string -> Token.T list
    29   val parse: Position.T -> string -> Toplevel.transition list
    30   val process_file: Path.T -> theory -> theory
    31   type isar
    32   val isar: bool -> isar
    33   val prepare_command: Position.T -> string -> Toplevel.transition
    34   val load_thy: string -> Position.T -> string list -> bool -> unit -> unit
    35 end;
    36 
    37 structure Outer_Syntax: OUTER_SYNTAX =
    38 struct
    39 
    40 (** outer syntax **)
    41 
    42 (* command parsers *)
    43 
    44 datatype command = Command of
    45  {comment: string,
    46   markup: ThyOutput.markup option,
    47   int_only: bool,
    48   parse: (Toplevel.transition -> Toplevel.transition) parser};
    49 
    50 fun make_command comment markup int_only parse =
    51   Command {comment = comment, markup = markup, int_only = int_only, parse = parse};
    52 
    53 
    54 (* parse command *)
    55 
    56 local
    57 
    58 fun terminate false = Scan.succeed ()
    59   | terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ());
    60 
    61 fun body cmd (name, _) =
    62   (case cmd name of
    63     SOME (Command {int_only, parse, ...}) =>
    64       Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
    65   | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
    66 
    67 in
    68 
    69 fun parse_command do_terminate cmd =
    70   Parse.semicolon >> K NONE ||
    71   Parse.sync >> K NONE ||
    72   (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
    73     >> (fn ((name, pos), (int_only, f)) =>
    74       SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
    75         Toplevel.interactive int_only |> f));
    76 
    77 end;
    78 
    79 
    80 
    81 (** global outer syntax **)
    82 
    83 local
    84 
    85 val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);
    86 val global_markups = Unsynchronized.ref ([]: (string * ThyOutput.markup) list);
    87 
    88 fun change_commands f = CRITICAL (fn () =>
    89  (Unsynchronized.change global_commands f;
    90   global_markups :=
    91     Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
    92       (! global_commands) []));
    93 
    94 in
    95 
    96 (* access current syntax *)
    97 
    98 fun get_commands () = ! global_commands;
    99 fun get_markups () = ! global_markups;
   100 
   101 fun get_command () = Symtab.lookup (get_commands ());
   102 fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), get_command ()));
   103 
   104 fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind;
   105 
   106 
   107 (* augment syntax *)
   108 
   109 fun add_command name kind cmd = CRITICAL (fn () =>
   110  (Keyword.command name kind;
   111   if not (Symtab.defined (get_commands ()) name) then ()
   112   else warning ("Redefining outer syntax command " ^ quote name);
   113   change_commands (Symtab.update (name, cmd))));
   114 
   115 fun command name comment kind parse =
   116   add_command name kind (make_command comment NONE false parse);
   117 
   118 fun markup_command markup name comment kind parse =
   119   add_command name kind (make_command comment (SOME markup) false parse);
   120 
   121 fun improper_command name comment kind parse =
   122   add_command name kind (make_command comment NONE true parse);
   123 
   124 end;
   125 
   126 fun internal_command name parse =
   127   command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
   128 
   129 
   130 (* local_theory commands *)
   131 
   132 fun local_theory_command do_print trans name comment kind parse =
   133   command name comment kind (Parse.opt_target -- parse
   134     >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
   135 
   136 val local_theory' = local_theory_command false Toplevel.local_theory';
   137 val local_theory = local_theory_command false Toplevel.local_theory;
   138 val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
   139 val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
   140 
   141 
   142 (* inspect syntax *)
   143 
   144 fun dest_commands () =
   145   get_commands () |> Symtab.dest |> sort_wrt #1
   146   |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
   147 
   148 fun print_outer_syntax () =
   149   let
   150     fun pretty_cmd (name, comment, _) =
   151       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   152     val (int_cmds, cmds) = List.partition #3 (dest_commands ());
   153   in
   154     [Pretty.strs ("syntax keywords:" :: map quote (Keyword.dest_keywords ())),
   155       Pretty.big_list "commands:" (map pretty_cmd cmds),
   156       Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
   157     |> Pretty.chunks |> Pretty.writeln
   158   end;
   159 
   160 
   161 
   162 (** toplevel parsing **)
   163 
   164 (* basic sources *)
   165 
   166 fun toplevel_source term do_recover cmd src =
   167   let
   168     val no_terminator =
   169       Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
   170     fun recover int =
   171       (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
   172   in
   173     src
   174     |> Token.source_proper
   175     |> Source.source Token.stopper
   176       (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
   177         (Option.map recover do_recover)
   178     |> Source.map_filter I
   179     |> Source.source Token.stopper
   180         (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
   181         (Option.map recover do_recover)
   182     |> Source.map_filter I
   183   end;
   184 
   185 
   186 (* off-line scanning/parsing *)
   187 
   188 fun scan pos str =
   189   Source.of_string str
   190   |> Symbol.source {do_recover = false}
   191   |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   192   |> Source.exhaust;
   193 
   194 fun parse pos str =
   195   Source.of_string str
   196   |> Symbol.source {do_recover = false}
   197   |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
   198   |> toplevel_source false NONE get_command
   199   |> Source.exhaust;
   200 
   201 
   202 (* process file *)
   203 
   204 fun process_file path thy =
   205   let
   206     val trs = parse (Path.position path) (File.read path);
   207     val init = Toplevel.init_theory "" (K thy) (K ()) Toplevel.empty;
   208     val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
   209   in
   210     (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
   211       (true, Context.Theory thy') => thy'
   212     | _ => error "Bad result state: global theory expected")
   213   end;
   214 
   215 
   216 (* interactive source of toplevel transformers *)
   217 
   218 type isar =
   219   (Toplevel.transition, (Toplevel.transition option,
   220     (Token.T, (Token.T option, (Token.T, (Token.T,
   221       (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
   222   Source.source) Source.source) Source.source) Source.source)
   223   Source.source) Source.source) Source.source) Source.source;
   224 
   225 fun isar term : isar =
   226   Source.tty
   227   |> Symbol.source {do_recover = true}
   228   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   229   |> toplevel_source term (SOME true) get_command;
   230 
   231 
   232 (* prepare toplevel commands -- fail-safe *)
   233 
   234 val not_singleton = "Exactly one command expected";
   235 
   236 fun prepare_span commands span =
   237   let
   238     val range_pos = Position.encode_range (ThySyntax.span_range span);
   239     val toks = ThySyntax.span_content span;
   240     val _ = List.app ThySyntax.report_token toks;
   241   in
   242     (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
   243       [tr] => (tr, true)
   244     | [] => (Toplevel.ignored range_pos, false)
   245     | _ => (Toplevel.malformed range_pos not_singleton, true))
   246     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   247   end;
   248 
   249 fun prepare_unit commands (cmd, proof, proper_proof) =
   250   let
   251     val (tr, proper_cmd) = prepare_span commands cmd;
   252     val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
   253   in
   254     if proper_cmd andalso proper_proof then [(tr, proof_trs)]
   255     else map (rpair []) (if proper_cmd then tr :: proof_trs else proof_trs)
   256   end;
   257 
   258 fun prepare_command pos str =
   259   let val (lexs, commands) = get_syntax () in
   260     (case ThySyntax.parse_spans lexs pos str of
   261       [span] => #1 (prepare_span commands span)
   262     | _ => Toplevel.malformed pos not_singleton)
   263   end;
   264 
   265 
   266 (* load_thy *)
   267 
   268 fun load_thy name pos text time =
   269   let
   270     val (lexs, commands) = get_syntax ();
   271 
   272     val _ = Present.init_theory name;
   273 
   274     val toks = Source.exhausted (ThySyntax.token_source lexs pos (Source.of_list text));
   275     val spans = Source.exhaust (ThySyntax.span_source toks);
   276     val _ = List.app ThySyntax.report_span spans;
   277     val units = Source.exhaust (ThySyntax.unit_source (Source.of_list spans))
   278       |> maps (prepare_unit commands);
   279 
   280     val _ = Present.theory_source name
   281       (fn () => HTML.html_mode (implode o map ThySyntax.present_span) spans);
   282 
   283     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
   284     val results = cond_timeit time "" (fn () => Toplevel.excursion units);
   285     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
   286 
   287     fun after_load () =
   288       ThyOutput.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
   289       |> Buffer.content
   290       |> Present.theory_output name;
   291   in after_load end;
   292 
   293 end;
   294