src/Pure/Isar/outer_syntax.ML
author wenzelm
Mon Sep 05 17:38:23 2005 +0200 (2005-09-05)
changeset 17265 12d99bb4304b
parent 17250 158ef530c153
child 17283 881f5873bac0
permissions -rw-r--r--
tuned check_text;
     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 -> 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 Symtab.curried_lookup (get_parsers ());
   129 
   130 fun command_tags name =
   131   (case Symtab.curried_lookup (get_parsers ()) name of
   132     SOME (((_, k), _), _) => OuterKeyword.tags_of k
   133   | NONE => []);
   134 
   135 fun is_markup kind name = (AList.lookup (op =) (! 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.curried_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 state = (IsarOutput.eval_antiquote (#1 (get_lexicons ())) state s; ());
   238 
   239 
   240 (* deps_thy *)
   241 
   242 fun deps_thy name ml path =
   243   let
   244     val src = Source.of_string (File.read path);
   245     val pos = Path.position path;
   246     val (name', parents, files) = ThyHeader.scan (src, pos);
   247     val ml_path = ThyLoad.ml_path name;
   248     val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
   249   in
   250     if name <> name' then
   251       error ("Filename " ^ quote (Path.pack path) ^
   252         " does not agree with theory name " ^ quote name')
   253     else (parents, map (Path.unpack o #1) files @ ml_file)
   254   end;
   255 
   256 
   257 (* load_thy *)
   258 
   259 local
   260 
   261 fun try_ml_file name time =
   262   let
   263     val path = ThyLoad.ml_path name;
   264     val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
   265     val tr_name = if time then "time_use" else "use";
   266   in
   267     if is_none (ThyLoad.check_file NONE path) then ()
   268     else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
   269   end;
   270 
   271 fun run_thy name path =
   272   let
   273     val pos = Path.position path;
   274     val text = Library.untabify (explode (File.read path));
   275     val text_src = Source.of_list text;
   276     fun present_text () = Source.exhaust (Symbol.source false text_src);
   277   in
   278     Present.init_theory name;
   279     Present.verbatim_source name present_text;
   280     if ThyHeader.is_old (text_src, pos) then
   281      (warning ("Non-Isar file format for theory " ^ quote name ^ " (deprecated)");
   282       ThySyn.load_thy name text;
   283       Present.old_symbol_source name present_text)   (*note: text presented twice*)
   284     else
   285       let
   286         val tok_src = text_src
   287           |> Symbol.source false
   288           |> T.source false (K (get_lexicons ())) pos
   289           |> Source.exhausted;
   290         val trs =
   291           tok_src
   292           |> toplevel_source false false false (K (get_parser ()))
   293           |> Source.exhaust;
   294       in
   295         IsarOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs tok_src
   296         |> Buffer.content
   297         |> Present.theory_output name
   298       end
   299   end;
   300 
   301 in
   302 
   303 fun load_thy name ml time path =
   304  (if time then
   305     timeit (fn () =>
   306      (writeln ("\n**** Starting theory " ^ quote name ^ " ****");
   307       run_thy name path;
   308       writeln ("**** Finished theory " ^ quote name ^ " ****\n")))
   309   else run_thy name path;
   310   Context.context (ThyInfo.get_theory name);
   311   if ml then try_ml_file name time else ());
   312 
   313 end;
   314 
   315 
   316 
   317 (** the read-eval-print loop **)
   318 
   319 (* main loop *)
   320 
   321 fun gen_loop term no_pos =
   322  (Context.reset_context ();
   323   Toplevel.loop (isar term no_pos);
   324   ml_prompts "ML> " "ML# ");
   325 
   326 fun gen_main term no_pos =
   327  (Toplevel.set_state Toplevel.toplevel;
   328   writeln (Session.welcome ());
   329   gen_loop term no_pos);
   330 
   331 structure Isar =
   332 struct
   333   fun main () = gen_main false false;
   334   fun loop () = gen_loop false false;
   335   fun sync_main () = gen_main true true;
   336   fun sync_loop () = gen_loop true true;
   337 end;
   338 
   339 
   340 (*final declarations of this structure!*)
   341 val command = parser false NONE;
   342 val markup_command = parser false o SOME;
   343 val improper_command = parser true NONE;
   344 
   345 end;
   346 
   347 (*setup theory syntax dependent operations*)
   348 ThyLoad.deps_thy_fn := OuterSyntax.deps_thy;
   349 ThyLoad.load_thy_fn := OuterSyntax.load_thy;
   350 structure ThyLoad: THY_LOAD = ThyLoad;
   351 
   352 structure BasicOuterSyntax: BASIC_OUTER_SYNTAX = OuterSyntax;
   353 open BasicOuterSyntax;
   354 open Isar;