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