# HG changeset patch
# User wenzelm
# Date 1230907473 -3600
# Node ID 4c830711e6f1296b23bba5df766daadaa3c7684a
# Parent  1a633304fa5e62fff58ad172bc48a242da588f0b
added type 'a parser, simplified signature;
added internal_command wrapper;
tuned;

diff -r 1a633304fa5e -r 4c830711e6f1 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Jan 02 15:44:33 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Jan 02 15:44:33 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/outer_syntax.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 The global Isabelle/Isar outer syntax.
@@ -10,17 +9,20 @@
 
 signature OUTER_SYNTAX =
 sig
-  type parser_fn = OuterLex.token list ->
-    (Toplevel.transition -> Toplevel.transition) * OuterLex.token list
-  val command: string -> string -> OuterKeyword.T -> parser_fn -> unit
-  val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T -> parser_fn -> unit
-  val improper_command: string -> string -> OuterKeyword.T -> parser_fn -> unit
+  type 'a parser = 'a OuterParse.parser
+  val command: string -> string -> OuterKeyword.T ->
+    (Toplevel.transition -> Toplevel.transition) parser -> unit
+  val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
+    (Toplevel.transition -> Toplevel.transition) parser -> unit
+  val improper_command: string -> string -> OuterKeyword.T ->
+    (Toplevel.transition -> Toplevel.transition) parser -> unit
+  val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
   val local_theory: string -> string -> OuterKeyword.T ->
-    (OuterParse.token list -> (local_theory -> local_theory) * OuterLex.token list) -> unit
+    (local_theory -> local_theory) parser -> unit
   val local_theory_to_proof': string -> string -> OuterKeyword.T ->
-    (OuterParse.token list -> (bool -> local_theory -> Proof.state) * OuterLex.token list) -> unit
+    (bool -> local_theory -> Proof.state) parser -> unit
   val local_theory_to_proof: string -> string -> OuterKeyword.T ->
-    (OuterParse.token list -> (local_theory -> Proof.state) * OuterLex.token list) -> unit
+    (local_theory -> Proof.state) parser -> unit
   val print_outer_syntax: unit -> unit
   val scan: Position.T -> string -> OuterLex.token list
   val parse: Position.T -> string -> Toplevel.transition list
@@ -36,22 +38,22 @@
 
 structure T = OuterLex;
 structure P = OuterParse;
+type 'a parser = 'a P.parser;
+
 
 
 (** outer syntax **)
 
-(* parsers *)
+(* command parsers *)
 
-type parser_fn = T.token list -> (Toplevel.transition -> Toplevel.transition) * T.token list;
-
-datatype parser = Parser of
+datatype command = Command of
  {comment: string,
   markup: ThyOutput.markup option,
   int_only: bool,
-  parse: parser_fn};
+  parse: (Toplevel.transition -> Toplevel.transition) parser};
 
-fun make_parser comment markup int_only parse =
-  Parser {comment = comment, markup = markup, int_only = int_only, parse = parse};
+fun make_command comment markup int_only parse =
+  Command {comment = comment, markup = markup, int_only = int_only, parse = parse};
 
 
 (* parse command *)
@@ -63,7 +65,7 @@
 
 fun body cmd (name, _) =
   (case cmd name of
-    SOME (Parser {int_only, parse, ...}) =>
+    SOME (Command {int_only, parse, ...}) =>
       P.!!! (Scan.prompt (name ^ "# ") (P.tags |-- parse >> pair int_only))
   | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
 
@@ -85,47 +87,50 @@
 
 local
 
-val global_parsers = ref (Symtab.empty: parser Symtab.table);
+val global_commands = ref (Symtab.empty: command Symtab.table);
 val global_markups = ref ([]: (string * ThyOutput.markup) list);
 
-fun change_parsers f = CRITICAL (fn () =>
- (change global_parsers f;
+fun change_commands f = CRITICAL (fn () =>
+ (change global_commands f;
   global_markups :=
-    Symtab.fold (fn (name, Parser {markup = SOME m, ...}) => cons (name, m) | _ => I)
-      (! global_parsers) []));
+    Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
+      (! global_commands) []));
 
 in
 
 (* access current syntax *)
 
-fun get_parsers () = CRITICAL (fn () => ! global_parsers);
+fun get_commands () = CRITICAL (fn () => ! global_commands);
 fun get_markups () = CRITICAL (fn () => ! global_markups);
 
-fun get_parser () = Symtab.lookup (get_parsers ());
-fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_parser ()));
+fun get_command () = Symtab.lookup (get_commands ());
+fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_command ()));
 
 fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind;
 
 
 (* augment syntax *)
 
-fun add_parser name kind parser = CRITICAL (fn () =>
+fun add_command name kind cmd = CRITICAL (fn () =>
  (OuterKeyword.command name kind;
-  if not (Symtab.defined (get_parsers ()) name) then ()
+  if not (Symtab.defined (get_commands ()) name) then ()
   else warning ("Redefining outer syntax command " ^ quote name);
-  change_parsers (Symtab.update (name, parser))));
+  change_commands (Symtab.update (name, cmd))));
 
 fun command name comment kind parse =
-  add_parser name kind (make_parser comment NONE false parse);
+  add_command name kind (make_command comment NONE false parse);
 
 fun markup_command markup name comment kind parse =
-  add_parser name kind (make_parser comment (SOME markup) false parse);
+  add_command name kind (make_command comment (SOME markup) false parse);
 
 fun improper_command name comment kind parse =
-  add_parser name kind (make_parser comment NONE true parse);
+  add_command name kind (make_command comment NONE true parse);
 
 end;
 
+fun internal_command name parse =
+  command name "(internal)" OuterKeyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
+
 
 (* local_theory commands *)
 
@@ -133,22 +138,22 @@
   command name comment kind (P.opt_target -- parse
     >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
 
-val local_theory           = local_theory_command false Toplevel.local_theory;
+val local_theory = local_theory_command false Toplevel.local_theory;
 val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
-val local_theory_to_proof  = local_theory_command true Toplevel.local_theory_to_proof;
+val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
 
 
 (* inspect syntax *)
 
-fun dest_parsers () =
-  get_parsers () |> Symtab.dest |> sort_wrt #1
-  |> map (fn (name, Parser {comment, int_only, ...}) => (name, comment, int_only));
+fun dest_commands () =
+  get_commands () |> Symtab.dest |> sort_wrt #1
+  |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
 
 fun print_outer_syntax () =
   let
     fun pretty_cmd (name, comment, _) =
       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
-    val (int_cmds, cmds) = List.partition #3 (dest_parsers ());
+    val (int_cmds, cmds) = List.partition #3 (dest_commands ());
   in
     [Pretty.strs ("syntax keywords:" :: map quote (OuterKeyword.dest_keywords ())),
       Pretty.big_list "commands:" (map pretty_cmd cmds),
@@ -194,7 +199,7 @@
   Source.of_string str
   |> Symbol.source {do_recover = false}
   |> T.source {do_recover = SOME false} OuterKeyword.get_lexicons pos
-  |> toplevel_source false NONE get_parser
+  |> toplevel_source false NONE get_command
   |> Source.exhaust;
 
 
@@ -225,39 +230,39 @@
   Source.tty
   |> Symbol.source {do_recover = true}
   |> T.source {do_recover = SOME true} OuterKeyword.get_lexicons Position.none
-  |> toplevel_source term (SOME true) get_parser;
+  |> toplevel_source term (SOME true) get_command;
 
 
 (* prepare toplevel commands -- fail-safe *)
 
 val not_singleton = "Exactly one command expected";
 
-fun prepare_span parser span =
+fun prepare_span commands span =
   let
     val range_pos = Position.encode_range (ThyEdit.span_range span);
     val toks = ThyEdit.span_content span;
     val _ = List.app ThyEdit.report_token toks;
   in
-    (case Source.exhaust (toplevel_source false NONE (K parser) (Source.of_list toks)) of
+    (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
       [tr] => (tr, true)
     | [] => (Toplevel.ignored range_pos, false)
     | _ => (Toplevel.malformed range_pos not_singleton, true))
     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   end;
 
-fun prepare_unit parser (cmd, proof, proper_proof) =
+fun prepare_unit commands (cmd, proof, proper_proof) =
   let
-    val (tr, proper_cmd) = prepare_span parser cmd;
-    val proof_trs = map (prepare_span parser) proof |> filter #2 |> map #1;
+    val (tr, proper_cmd) = prepare_span commands cmd;
+    val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
   in
     if proper_cmd andalso proper_proof then [(tr, proof_trs)]
     else map (rpair []) (if proper_cmd then tr :: proof_trs else proof_trs)
   end;
 
 fun prepare_command pos str =
-  let val (lexs, parser) = get_syntax () in
+  let val (lexs, commands) = get_syntax () in
     (case ThyEdit.parse_spans lexs pos str of
-      [span] => #1 (prepare_span parser span)
+      [span] => #1 (prepare_span commands span)
     | _ => Toplevel.malformed pos not_singleton)
   end;
 
@@ -266,7 +271,7 @@
 
 fun load_thy name pos text time =
   let
-    val (lexs, parser) = get_syntax ();
+    val (lexs, commands) = get_syntax ();
 
     val _ = Present.init_theory name;
 
@@ -274,7 +279,7 @@
     val spans = Source.exhaust (ThyEdit.span_source toks);
     val _ = List.app ThyEdit.report_span spans;
     val units = Source.exhaust (ThyEdit.unit_source (Source.of_list spans))
-      |> maps (prepare_unit parser);
+      |> maps (prepare_unit commands);
 
     val _ = Present.theory_source name
       (fn () => HTML.html_mode (implode o map ThyEdit.present_span) spans);