src/Pure/Isar/outer_syntax.ML
author wenzelm
Wed Jun 25 17:38:32 2008 +0200 (2008-06-25)
changeset 27353 71c4dd53d4cb
parent 26990 a91f7741967a
child 27439 7d5c4e73c89e
permissions -rw-r--r--
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
     1 (*  Title:      Pure/Isar/outer_syntax.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 The global Isabelle/Isar outer syntax.
     6 
     7 Note: the syntax for files is statically determined at the very
     8 beginning; for interactive processing it may change dynamically.
     9 *)
    10 
    11 signature OUTER_SYNTAX =
    12 sig
    13   type parser_fn = OuterLex.token list ->
    14     (Toplevel.transition -> Toplevel.transition) * OuterLex.token list
    15   val command: string -> string -> OuterKeyword.T -> parser_fn -> unit
    16   val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T -> parser_fn -> unit
    17   val improper_command: string -> string -> OuterKeyword.T -> parser_fn -> unit
    18   val local_theory: string -> string -> OuterKeyword.T ->
    19     (OuterParse.token list -> (local_theory -> local_theory) * OuterLex.token list) -> unit
    20   val local_theory_to_proof': string -> string -> OuterKeyword.T ->
    21     (OuterParse.token list -> (bool -> local_theory -> Proof.state) * OuterLex.token list) -> unit
    22   val local_theory_to_proof: string -> string -> OuterKeyword.T ->
    23     (OuterParse.token list -> (local_theory -> Proof.state) * OuterLex.token list) -> unit
    24   val print_outer_syntax: unit -> unit
    25   val scan: string -> OuterLex.token list
    26   val parse: Position.T -> string -> Toplevel.transition list
    27   val process_file: Path.T -> theory -> theory
    28   type isar
    29   val isar: bool -> isar
    30   val load_thy: Path.T -> string -> Position.T -> string list -> bool -> unit
    31 end;
    32 
    33 structure OuterSyntax: OUTER_SYNTAX =
    34 struct
    35 
    36 structure T = OuterLex;
    37 structure P = OuterParse;
    38 
    39 
    40 (** outer syntax **)
    41 
    42 (* parsers *)
    43 
    44 type parser_fn = T.token list -> (Toplevel.transition -> Toplevel.transition) * T.token list;
    45 
    46 datatype parser = Parser of
    47  {comment: string,
    48   markup: ThyOutput.markup option,
    49   int_only: bool,
    50   parse: parser_fn};
    51 
    52 fun make_parser comment markup int_only parse =
    53   Parser {comment = comment, markup = markup, int_only = int_only, parse = parse};
    54 
    55 
    56 (* parse command *)
    57 
    58 local
    59 
    60 fun terminate false = Scan.succeed ()
    61   | terminate true = P.group "end of input" (Scan.option P.sync -- P.semicolon >> K ());
    62 
    63 fun body cmd (name, _) =
    64   (case cmd name of
    65     SOME (Parser {int_only, parse, ...}) =>
    66       P.!!! (Scan.prompt (name ^ "# ") (P.tags |-- parse >> pair int_only))
    67   | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
    68 
    69 in
    70 
    71 fun parse_command do_terminate cmd =
    72   P.semicolon >> K NONE ||
    73   P.sync >> K NONE ||
    74   (P.position P.command :-- body cmd) --| terminate do_terminate
    75     >> (fn ((name, pos), (int_only, f)) =>
    76       SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
    77         Toplevel.interactive int_only |> f));
    78 
    79 end;
    80 
    81 
    82 
    83 (** global outer syntax **)
    84 
    85 local
    86 
    87 val global_parsers = ref (Symtab.empty: parser Symtab.table);
    88 val global_markups = ref ([]: (string * ThyOutput.markup) list);
    89 
    90 fun change_parsers f = CRITICAL (fn () =>
    91  (change global_parsers f;
    92   global_markups :=
    93     Symtab.fold (fn (name, Parser {markup = SOME m, ...}) => cons (name, m) | _ => I)
    94       (! global_parsers) []));
    95 
    96 in
    97 
    98 (* access current syntax *)
    99 
   100 fun get_parsers () = CRITICAL (fn () => ! global_parsers);
   101 fun get_markups () = CRITICAL (fn () => ! global_markups);
   102 
   103 fun get_parser () = Symtab.lookup (get_parsers ());
   104 
   105 fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind;
   106 
   107 
   108 (* augment syntax *)
   109 
   110 fun add_parser name kind parser = CRITICAL (fn () =>
   111  (OuterKeyword.command name kind;
   112   if not (Symtab.defined (get_parsers ()) name) then ()
   113   else warning ("Redefining outer syntax command " ^ quote name);
   114   change_parsers (Symtab.update (name, parser))));
   115 
   116 fun command name comment kind parse =
   117   add_parser name kind (make_parser comment NONE false parse);
   118 
   119 fun markup_command markup name comment kind parse =
   120   add_parser name kind (make_parser comment (SOME markup) false parse);
   121 
   122 fun improper_command name comment kind parse =
   123   add_parser name kind (make_parser comment NONE true parse);
   124 
   125 end;
   126 
   127 
   128 (* local_theory commands *)
   129 
   130 fun local_theory_command do_print trans name comment kind parse =
   131   command name comment kind (P.opt_target -- parse
   132     >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
   133 
   134 val local_theory           = local_theory_command false Toplevel.local_theory;
   135 val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
   136 val local_theory_to_proof  = local_theory_command true Toplevel.local_theory_to_proof;
   137 
   138 
   139 (* inspect syntax *)
   140 
   141 fun dest_parsers () =
   142   get_parsers () |> Symtab.dest |> sort_wrt #1
   143   |> map (fn (name, Parser {comment, int_only, ...}) => (name, comment, int_only));
   144 
   145 fun print_outer_syntax () =
   146   let
   147     fun pretty_cmd (name, comment, _) =
   148       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   149     val (int_cmds, cmds) = List.partition #3 (dest_parsers ());
   150   in
   151     [Pretty.strs ("syntax keywords:" :: map quote (OuterKeyword.dest_keywords ())),
   152       Pretty.big_list "commands:" (map pretty_cmd cmds),
   153       Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
   154     |> Pretty.chunks |> Pretty.writeln
   155   end;
   156 
   157 
   158 
   159 (** toplevel parsing **)
   160 
   161 (* basic sources *)
   162 
   163 fun toplevel_source term do_recover cmd src =
   164   let
   165     val no_terminator =
   166       Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
   167     fun recover int =
   168       (int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
   169   in
   170     src
   171     |> T.source_proper
   172     |> Source.source T.stopper
   173       (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME))
   174         (Option.map recover do_recover)
   175     |> Source.map_filter I
   176     |> Source.source T.stopper
   177         (Scan.bulk (fn xs => P.!!! (parse_command term (cmd ())) xs))
   178         (Option.map recover do_recover)
   179     |> Source.map_filter I
   180   end;
   181 
   182 
   183 (* off-line scanning/parsing *)
   184 
   185 fun scan str =
   186   Source.of_string str
   187   |> Symbol.source false
   188   |> T.source (SOME false) OuterKeyword.get_lexicons Position.none
   189   |> Source.exhaust;
   190 
   191 fun parse pos str =
   192   Source.of_string str
   193   |> Symbol.source false
   194   |> T.source (SOME false) OuterKeyword.get_lexicons pos
   195   |> toplevel_source false NONE get_parser
   196   |> Source.exhaust;
   197 
   198 
   199 (* process file *)
   200 
   201 fun process_file path thy =
   202   let
   203     val result = ref thy;
   204     val trs = parse (Path.position path) (File.read path);
   205     val init = Toplevel.init_theory (K thy) (fn thy' => result := thy') (K ());
   206     val _ = Toplevel.excursion (init Toplevel.empty :: trs @ [Toplevel.exit Toplevel.empty]);
   207   in ! result end;
   208 
   209 
   210 (* interactive source of toplevel transformers *)
   211 
   212 type isar =
   213   (Toplevel.transition, (Toplevel.transition option,
   214     (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
   215       Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source)
   216           Source.source) Source.source) Source.source) Source.source) Source.source) Source.source;
   217 
   218 fun isar term : isar =
   219   Source.tty
   220   |> Symbol.source true
   221   |> T.source (SOME true) OuterKeyword.get_lexicons Position.none
   222   |> toplevel_source term (SOME true) get_parser;
   223 
   224 
   225 (* load_thy *)
   226 
   227 fun load_thy dir name pos text time =
   228   let
   229     val text_src = Source.of_list (Library.untabify text);
   230     val (lexs, parser) = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_parser ()));
   231 
   232     val _ = Present.init_theory name;
   233     val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text_src));
   234     val toks = text_src
   235       |> Symbol.source false
   236       |> T.source NONE (K lexs) pos
   237       |> Source.exhausted;
   238     val trs = toks
   239       |> toplevel_source false NONE (K parser)
   240       |> Source.exhaust;
   241 
   242     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
   243     val _ = cond_timeit time "" (fn () =>
   244       ThyOutput.process_thy (#1 lexs) OuterKeyword.command_tags is_markup trs toks
   245       |> Buffer.content
   246       |> Present.theory_output name);
   247     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
   248   in () end;
   249 
   250 end;
   251