src/Pure/Isar/outer_syntax.ML
author wenzelm
Thu Aug 18 12:07:33 2005 +0200 (2005-08-18)
changeset 17118 1ff59b7b35b7
parent 17071 f753d6dd9bd0
child 17184 3d80209e9a53
permissions -rw-r--r--
fixed command prompt (was broken due to P.tags);
     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 
     8 signature BASIC_OUTER_SYNTAX =
     9 sig
    10   structure Isar:
    11     sig
    12       val main: unit -> unit
    13       val loop: unit -> unit
    14       val sync_main: unit -> unit
    15       val sync_loop: unit -> unit
    16     end;
    17 end;
    18 
    19 signature OUTER_SYNTAX =
    20 sig
    21   include BASIC_OUTER_SYNTAX
    22   type token
    23   type parser
    24   val command: string -> string -> OuterKeyword.T ->
    25     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    26   val markup_command: IsarOutput.markup -> string -> string -> OuterKeyword.T ->
    27     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    28   val improper_command: string -> string -> OuterKeyword.T ->
    29     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    30   val is_keyword: string -> bool
    31   val dest_keywords: unit -> string list
    32   val dest_parsers: unit -> (string * string * string * bool) list
    33   val print_outer_syntax: unit -> unit
    34   val print_commands: Toplevel.transition -> Toplevel.transition
    35   val add_keywords: string list -> unit
    36   val add_parsers: parser list -> unit
    37   val check_text: string * Position.T -> bool -> Toplevel.state -> unit
    38   val deps_thy: string -> bool -> Path.T -> string list * Path.T list
    39   val load_thy: string -> bool -> bool -> Path.T -> unit
    40   val isar: bool -> bool -> unit Toplevel.isar
    41   val scan: string -> OuterLex.token list
    42   val read: OuterLex.token list -> (string * OuterLex.token list * Toplevel.transition) list
    43 end;
    44 
    45 structure OuterSyntax : OUTER_SYNTAX  =
    46 struct
    47 
    48 structure T = OuterLex;
    49 structure P = OuterParse;
    50 
    51 
    52 (** outer syntax **)
    53 
    54 (* parsers *)
    55 
    56 type token = T.token;
    57 type parser_fn = token list -> (Toplevel.transition -> Toplevel.transition) * token list;
    58 
    59 datatype parser =
    60   Parser of string * (string * OuterKeyword.T * IsarOutput.markup option) * bool * parser_fn;
    61 
    62 fun parser int_only markup name comment kind parse =
    63   Parser (name, (comment, kind, markup), int_only, parse);
    64 
    65 
    66 (* parse command *)
    67 
    68 local
    69 
    70 fun terminate false = Scan.succeed ()
    71   | terminate true = P.group "end of input" (Scan.option P.sync -- P.semicolon >> K ());
    72 
    73 fun trace false parse = parse
    74   | trace true parse = Scan.trace parse >> (fn (f, toks) => f o Toplevel.source toks);
    75 
    76 fun body cmd do_trace (name, _) =
    77   (case cmd name of
    78     SOME (int_only, parse) =>
    79       P.!!! (Scan.prompt (name ^ "# ") (trace do_trace (P.tags |-- parse) >> pair int_only))
    80   | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
    81 
    82 in
    83 
    84 fun command do_terminate do_trace cmd =
    85   P.semicolon >> K NONE ||
    86   P.sync >> K NONE ||
    87   (P.position P.command :-- body cmd do_trace) --| terminate do_terminate
    88     >> (fn ((name, pos), (int_only, f)) =>
    89       SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
    90         Toplevel.interactive int_only |> f));
    91 
    92 end;
    93 
    94 
    95 
    96 (** global outer syntax **)
    97 
    98 local
    99 
   100 val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
   101 val global_parsers =
   102   ref (Symtab.empty: (((string * OuterKeyword.T) * (bool * parser_fn)) * IsarOutput.markup option)
   103     Symtab.table);
   104 val global_markups = ref ([]: (string * IsarOutput.markup) list);
   105 
   106 fun change_lexicons f =
   107   let val lexs = f (! global_lexicons) in
   108     (case (op inter_string) (pairself Scan.dest_lexicon lexs) of
   109       [] => global_lexicons := lexs
   110     | bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads))
   111   end;
   112 
   113 fun make_markups () = global_markups :=
   114   Symtab.fold (fn (name, (_, SOME m)) => cons (name, m) | _ => I) (! global_parsers) [];
   115 
   116 fun change_parsers f = (Library.change global_parsers f; make_markups ());
   117 
   118 in
   119 
   120 
   121 (* access current syntax *)
   122 
   123 (*Note: the syntax for files is statically determined at the very
   124   beginning; for interactive processing it may change dynamically.*)
   125 
   126 fun get_lexicons () = ! global_lexicons;
   127 fun get_parsers () = ! global_parsers;
   128 fun get_parser () = Option.map (#2 o #1) o curry Symtab.lookup (get_parsers ());
   129 
   130 fun command_tags name =
   131   (case Symtab.lookup (get_parsers (), name) of
   132     SOME (((_, k), _), _) => OuterKeyword.tags_of k
   133   | NONE => []);
   134 
   135 fun is_markup kind name = (assoc_string (! global_markups, name) = SOME kind);
   136 
   137 
   138 (* augment syntax *)
   139 
   140 fun add_keywords keywords = change_lexicons (apfst (fn lex =>
   141   (Scan.extend_lexicon lex (map Symbol.explode keywords))));
   142 
   143 fun add_parser (Parser (name, (comment, kind, markup), int_only, parse)) tab =
   144  (if not (Symtab.defined tab name) then ()
   145   else warning ("Redefined outer syntax command " ^ quote name);
   146   Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab));
   147 
   148 fun add_parsers parsers =
   149   (change_parsers (fold add_parser parsers);
   150     change_lexicons (apsnd (fn lex => Scan.extend_lexicon lex
   151       (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers))));
   152 
   153 end;
   154 
   155 
   156 (* print syntax *)
   157 
   158 fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
   159 fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ()));
   160 
   161 fun dest_parsers () =
   162   get_parsers () |> Symtab.dest |> sort_wrt #1
   163   |> map (fn (name, (((cmt, kind), (int_only, _)), _)) =>
   164     (name, cmt, OuterKeyword.kind_of kind, int_only));
   165 
   166 fun print_outer_syntax () =
   167   let
   168     fun pretty_cmd (name, comment, _, _) =
   169       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   170     val (int_cmds, cmds) = List.partition #4 (dest_parsers ());
   171   in
   172     [Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())),
   173       Pretty.big_list "proper commands:" (map pretty_cmd cmds),
   174       Pretty.big_list "improper commands (interactive-only):" (map pretty_cmd int_cmds)]
   175     |> Pretty.chunks |> Pretty.writeln
   176   end;
   177 
   178 val print_commands = Toplevel.imperative print_outer_syntax;
   179 
   180 
   181 
   182 (** toplevel parsing **)
   183 
   184 (* basic sources *)
   185 
   186 fun toplevel_source term do_trace do_recover cmd src =
   187   let
   188     val no_terminator =
   189       Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
   190     fun recover x = (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]) x;
   191   in
   192     src
   193     |> T.source_proper
   194     |> Source.source T.stopper
   195       (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME))
   196       (if do_recover then SOME recover else NONE)
   197     |> Source.mapfilter I
   198     |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term do_trace (cmd ())) xs))
   199       (if do_recover then SOME recover else NONE)
   200     |> Source.mapfilter I
   201   end;
   202 
   203 
   204 (* interactive source of toplevel transformers *)
   205 
   206 fun isar term no_pos =
   207   Source.tty
   208   |> Symbol.source true
   209   |> T.source true get_lexicons
   210     (if no_pos then Position.none else Position.line_name 1 "stdin")
   211   |> toplevel_source term false true get_parser;
   212 
   213 
   214 (* scan text *)
   215 
   216 fun scan str =
   217   Source.of_string str
   218   |> Symbol.source false
   219   |> T.source true get_lexicons Position.none
   220   |> Source.exhaust;
   221 
   222 
   223 (* read tokens with trace *)
   224 
   225 fun read toks =
   226   Source.of_list toks
   227   |> toplevel_source false true true get_parser
   228   |> Source.exhaust
   229   |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
   230 
   231 
   232 
   233 (** read theory **)
   234 
   235 (* check_text *)
   236 
   237 fun check_text s true state = (IsarOutput.eval_antiquote (#1 (get_lexicons ())) state s; ())
   238   | check_text _ false _ = ();
   239 
   240 
   241 (* deps_thy *)
   242 
   243 fun deps_thy name ml path =
   244   let
   245     val src = Source.of_string (File.read path);
   246     val pos = Path.position path;
   247     val (name', parents, files) = ThyHeader.scan (src, pos);
   248     val ml_path = ThyLoad.ml_path name;
   249     val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
   250   in
   251     if name <> name' then
   252       error ("Filename " ^ quote (Path.pack path) ^
   253         " does not agree with theory name " ^ quote name')
   254     else (parents, map (Path.unpack o #1) files @ ml_file)
   255   end;
   256 
   257 
   258 (* load_thy *)
   259 
   260 local
   261 
   262 fun try_ml_file name time =
   263   let
   264     val path = ThyLoad.ml_path name;
   265     val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
   266     val tr_name = if time then "time_use" else "use";
   267   in
   268     if is_none (ThyLoad.check_file NONE path) then ()
   269     else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
   270   end;
   271 
   272 fun run_thy name path =
   273   let
   274     val pos = Path.position path;
   275     val text = Library.untabify (explode (File.read path));
   276     val text_src = Source.of_list text;
   277     fun present_text () = Source.exhaust (Symbol.source false text_src);
   278   in
   279     Present.init_theory name;
   280     Present.verbatim_source name present_text;
   281     if ThyHeader.is_old (text_src, pos) then (ThySyn.load_thy name text;
   282       Present.old_symbol_source name present_text)   (*note: text presented twice*)
   283     else
   284       let
   285         val tok_src = text_src
   286           |> Symbol.source false
   287           |> T.source false (K (get_lexicons ())) pos
   288           |> Source.exhausted;
   289         val trs =
   290           tok_src
   291           |> toplevel_source false false false (K (get_parser ()))
   292           |> Source.exhaust;
   293       in
   294         IsarOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs tok_src
   295         |> Buffer.content
   296         |> Present.theory_output name
   297       end
   298   end;
   299 
   300 in
   301 
   302 fun load_thy name ml time path =
   303  (if time then
   304     timeit (fn () =>
   305      (writeln ("\n**** Starting theory " ^ quote name ^ " ****");
   306       run_thy name path;
   307       writeln ("**** Finished theory " ^ quote name ^ " ****\n")))
   308   else run_thy name path;
   309   Context.context (ThyInfo.get_theory name);
   310   if ml then try_ml_file name time else ());
   311 
   312 end;
   313 
   314 
   315 
   316 (** the read-eval-print loop **)
   317 
   318 (* main loop *)
   319 
   320 fun gen_loop term no_pos =
   321  (Context.reset_context ();
   322   Toplevel.loop (isar term no_pos);
   323   ml_prompts "ML> " "ML# ");
   324 
   325 fun gen_main term no_pos =
   326  (Toplevel.set_state Toplevel.toplevel;
   327   writeln (Session.welcome ());
   328   gen_loop term no_pos);
   329 
   330 structure Isar =
   331 struct
   332   fun main () = gen_main false false;
   333   fun loop () = gen_loop false false;
   334   fun sync_main () = gen_main true true;
   335   fun sync_loop () = gen_loop true true;
   336 end;
   337 
   338 
   339 (*final declarations of this structure!*)
   340 val command = parser false NONE;
   341 val markup_command = parser false o SOME;
   342 val improper_command = parser true NONE;
   343 
   344 end;
   345 
   346 (*setup theory syntax dependent operations*)
   347 ThyLoad.deps_thy_fn := OuterSyntax.deps_thy;
   348 ThyLoad.load_thy_fn := OuterSyntax.load_thy;
   349 structure ThyLoad: THY_LOAD = ThyLoad;
   350 
   351 structure BasicOuterSyntax: BASIC_OUTER_SYNTAX = OuterSyntax;
   352 open BasicOuterSyntax;
   353 open Isar;