separate command tokens;

--- a/src/Pure/Isar/outer_lex.ML	Fri Jul 16 22:25:07 1999 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Fri Jul 16 22:26:44 1999 +0200
@@ -8,8 +8,8 @@
 signature OUTER_LEX =
 sig
   datatype token_kind =
-    Keyword | Ident | LongIdent | SymIdent | Var | TextVar | TypeIdent | TypeVar | Nat |
-    String | Verbatim | Ignore | Sync | EOF
+    Command | Keyword | Ident | LongIdent | SymIdent | Var | TextVar | TypeIdent | TypeVar |
+    Nat | String | Verbatim | Ignore | Sync | EOF
   type token
   val str_of_kind: token_kind -> string
   val stopper: token * (token -> bool)
@@ -18,14 +18,15 @@
   val position_of: token -> Position.T
   val pos_of: token -> string
   val is_kind: token_kind -> token -> bool
-  val keyword_pred: (string -> bool) -> token -> bool
+  val keyword_with: (string -> bool) -> token -> bool
   val name_of: token -> string
   val is_proper: token -> bool
   val val_of: token -> string
   val is_sid: string -> bool
-  val scan: Scan.lexicon ->
+  val scan: (Scan.lexicon * Scan.lexicon) ->
     Position.T * Symbol.symbol list -> token * (Position.T * Symbol.symbol list)
-  val source: bool -> (unit -> Scan.lexicon) -> Position.T -> (Symbol.symbol, 'a) Source.source ->
+  val source: bool -> (unit -> (Scan.lexicon * Scan.lexicon)) ->
+    Position.T -> (Symbol.symbol, 'a) Source.source ->
     (token, (token, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
 end;
 
@@ -38,13 +39,14 @@
 (* datatype token *)
 
 datatype token_kind =
-  Keyword | Ident | LongIdent | SymIdent | Var | TextVar | TypeIdent | TypeVar | Nat |
-  String | Verbatim | Ignore | Sync | EOF;
+  Command | Keyword | Ident | LongIdent | SymIdent | Var | TextVar | TypeIdent | TypeVar |
+  Nat | String | Verbatim | Ignore | Sync | EOF;
 
 datatype token = Token of Position.T * (token_kind * string);
 
 val str_of_kind =
- fn Keyword => "keyword"
+ fn Command => "command"
+  | Keyword => "keyword"
   | Ident => "identifier"
   | LongIdent => "long identifier"
   | SymIdent => "symbolic identifier"
@@ -87,8 +89,8 @@
 
 fun is_kind k (Token (_, (k', _))) = k = k';
 
-fun keyword_pred pred (Token (_, (Keyword, x))) = pred x
-  | keyword_pred _ _ = false;
+fun keyword_with pred (Token (_, (Keyword, x))) = pred x
+  | keyword_with _ _ = false;
 
 fun name_of (Token (_, (k, _))) = str_of_kind k;
 
@@ -189,7 +191,7 @@
 
 (* scan token *)
 
-fun scan lex (pos, cs) =
+fun scan (lex1, lex2) (pos, cs) =
   let
     fun token k x = Token (pos, (k, x));
     fun ignore _ = token Ignore "";
@@ -202,7 +204,9 @@
       scan_comment >> ignore ||
       keep_line (Scan.one Symbol.is_sync >> sync) ||
       keep_line (Scan.max token_leq
-        (Scan.literal lex >> (token Keyword o implode))
+        (Scan.max token_leq
+          (Scan.literal lex1 >> (token Keyword o implode))
+          (Scan.literal lex2 >> (token Command o implode)))
         (Syntax.scan_longid >> token LongIdent ||
           Syntax.scan_id >> token Ident ||
           Syntax.scan_var >> token Var ||

--- a/src/Pure/Isar/outer_parse.ML	Fri Jul 16 22:25:07 1999 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Fri Jul 16 22:26:44 1999 +0200
@@ -12,6 +12,7 @@
   val !!! : (token list -> 'a) -> token list -> 'a
   val $$$ : string -> token list -> string * token list
   val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
+  val command: token list -> string * token list
   val keyword: token list -> string * token list
   val short_ident: token list -> string * token list
   val long_ident: token list -> string * token list
@@ -114,6 +115,7 @@
   group (OuterLex.str_of_kind k)
     (Scan.one (OuterLex.is_kind k) >> OuterLex.val_of);
 
+val command = kind OuterLex.Command;
 val keyword = kind OuterLex.Keyword;
 val short_ident = kind OuterLex.Ident;
 val long_ident = kind OuterLex.LongIdent;
@@ -130,8 +132,7 @@
 
 fun $$$ x =
   group (OuterLex.str_of_kind OuterLex.Keyword ^ " " ^ quote x)
-    (Scan.one (OuterLex.is_kind OuterLex.Keyword andf (equal x o OuterLex.val_of))
-      >> OuterLex.val_of);
+    (Scan.one (OuterLex.keyword_with (equal x)) >> OuterLex.val_of);
 
 val nat = number >> (fst o Term.read_int o Symbol.explode);
 
@@ -238,7 +239,7 @@
 
 (* arguments *)
 
-fun keyword_symid is_symid = Scan.one (OuterLex.keyword_pred is_symid) >> OuterLex.val_of;
+fun keyword_symid is_symid = Scan.one (OuterLex.keyword_with is_symid) >> OuterLex.val_of;
 
 fun atom_arg is_symid blk =
   group "argument"

--- a/src/Pure/Isar/outer_syntax.ML	Fri Jul 16 22:25:07 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Jul 16 22:26:44 1999 +0200
@@ -3,10 +3,6 @@
     Author:     Markus Wenzel, TU Muenchen
 
 The global Isabelle/Isar outer syntax.
-
-TODO:
-  - cleanup;
-  - avoid string constants;
 *)
 
 signature BASIC_OUTER_SYNTAX =
@@ -46,7 +42,8 @@
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val improper_command: string -> string -> string ->
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
-  val dest_syntax: unit -> string list * (string * string) list
+  val dest_keywords: unit -> string list
+  val dest_parsers: unit -> (string * string * string * bool) list
   val print_outer_syntax: unit -> unit
   val add_keywords: string list -> unit
   val add_parsers: parser list -> unit
@@ -104,13 +101,10 @@
 
 local
 
-fun command_name cmd =
-  P.group "command"
-    (P.position (Scan.one (OuterLex.keyword_pred (is_some o cmd)) >> OuterLex.val_of));
-
 fun command_body cmd (name, _) =
-  let val (int_only, parse) = the (cmd name)
-  in P.!!! (Scan.prompt (name ^ "# ") (parse >> pair int_only)) end;
+  (case cmd name of
+    Some (int_only, parse) => P.!!! (Scan.prompt (name ^ "# ") (parse >> pair int_only))
+  | None => sys_error ("no parser for outer syntax command " ^ quote name));
 
 fun terminator false = Scan.succeed ()
   | terminator true = P.group "terminator" (Scan.option P.sync -- P.$$$ ";" >> K ());
@@ -120,7 +114,7 @@
 fun command term cmd =
   P.$$$ ";" >> K None ||
   P.sync >> K None ||
-  (command_name cmd :-- command_body cmd) --| terminator term
+  (P.position P.command :-- command_body cmd) --| terminator term
     >> (fn ((name, pos), (int_only, f)) =>
       Some (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
         Toplevel.interactive int_only |> f));
@@ -131,34 +125,36 @@
 
 (** global syntax state **)
 
-val global_lexicon = ref Scan.empty_lexicon;
+local
+
+val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
 val global_parsers = ref (Symtab.empty: ((string * string) * (bool * parser_fn)) Symtab.table);
 
-
-(* print syntax *)
+fun change_lexicons f =
+  let val lexs = f (! global_lexicons) in
+    (case (op inter_string) (pairself Scan.dest_lexicon lexs) of
+      [] => global_lexicons := lexs
+    | bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads))
+  end;
 
-fun dest_syntax () =
-  (map implode (Scan.dest_lexicon (! global_lexicon)),
-    map (fn (name, ((_, kind), _)) => (name, kind)) (Symtab.dest (! global_parsers)));
+fun change_parsers f = global_parsers := f (! global_parsers);
 
-fun print_outer_syntax () =
-  let
-    val keywords = map implode (Scan.dest_lexicon (! global_lexicon));
-    fun pretty_cmd (name, ((comment, _), _)) =
-      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
-    val (int_cmds, cmds) = partition (#1 o #2 o #2) (Symtab.dest (! global_parsers));
-  in
-    Pretty.writeln (Pretty.strs ("syntax keywords:" :: map quote keywords));
-    Pretty.writeln (Pretty.big_list "proper commands:" (map pretty_cmd cmds));
-    Pretty.writeln (Pretty.big_list "improper commands (interactive-only):"
-      (map pretty_cmd int_cmds))
-  end;
+in
+
+(* get current lexers / parsers *)
+
+(*Note: the syntax for files is statically determined at the very
+  beginning; for interactive processing it may change dynamically.*)
+
+fun get_lexicons () = ! global_lexicons;
+fun get_parsers () = ! global_parsers;
+fun get_parser () = apsome snd o curry Symtab.lookup (! global_parsers);
 
 
 (* augment syntax *)
 
-fun add_keywords keywords =
-  global_lexicon := Scan.extend_lexicon (! global_lexicon) (map Symbol.explode keywords);
+fun add_keywords keywords = change_lexicons (apfst (fn lex =>
+  (Scan.extend_lexicon lex (map Symbol.explode keywords))));
 
 fun add_parser (tab, Parser (name, comment, int_only, parse)) =
  (if is_none (Symtab.lookup (tab, name)) then ()
@@ -166,17 +162,32 @@
   Symtab.update ((name, (comment, (int_only, parse))), tab));
 
 fun add_parsers parsers =
-  (global_parsers := foldl add_parser (! global_parsers, parsers);
-    add_keywords (map (fn Parser (name, _, _, _) => name) parsers));
+  (change_parsers (fn tab => foldl add_parser (tab, parsers));
+    change_lexicons (apsnd (fn lex => Scan.extend_lexicon lex
+      (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers))));
+
+end;
 
 
-(* get current lexer / parser *)
+(* print syntax *)
+
+fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ()));
+
+fun dest_parsers () =
+  map (fn (name, ((cmt, kind), (int_only, _))) => (name, cmt, kind, int_only))
+    (Symtab.dest (get_parsers ()));
 
-(*Note: the syntax for files is statically determined at the very
-  beginning; for interactive processing it may change dynamically.*)
-
-fun get_lexicon () = ! global_lexicon;
-fun get_parser () = apsome snd o curry Symtab.lookup (! global_parsers);
+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) = partition #4 (dest_parsers ());
+  in
+    Pretty.writeln (Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())));
+    Pretty.writeln (Pretty.big_list "proper commands:" (map pretty_cmd cmds));
+    Pretty.writeln (Pretty.big_list "improper commands (interactive-only):"
+      (map pretty_cmd int_cmds))
+  end;
 
 
 
@@ -211,10 +222,10 @@
 
 (* detect header *)
 
-fun scan_header get_lexicon scan (src, pos) =
+fun scan_header get_lex scan (src, pos) =
   src
   |> Symbol.source false
-  |> OuterLex.source false get_lexicon pos
+  |> OuterLex.source false (fn () => (get_lex (), Scan.empty_lexicon)) pos
   |> Source.source OuterLex.stopper (Scan.single scan) None
   |> (fst o the o Source.get_single);
 
@@ -237,7 +248,8 @@
 
 local
 
-val file_name = (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
+val file_name =
+  (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
 
 val theory_head =
   (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name) --
@@ -291,7 +303,7 @@
     val lex_src =
       src
       |> Symbol.source false
-      |> OuterLex.source false (K (get_lexicon ())) pos;
+      |> OuterLex.source false (K (get_lexicons ())) pos;
     val only_head =
       lex_src
       |> Source.source OuterLex.stopper (Scan.single (Scan.option only_header)) None
@@ -331,7 +343,7 @@
 fun isar term =
   Source.tty
   |> Symbol.source true
-  |> OuterLex.source true get_lexicon (Position.line_name 1 "stdin")
+  |> OuterLex.source true get_lexicons (Position.line_name 1 "stdin")
   |> source term true get_parser;