# HG changeset patch
# User wenzelm
# Date 1331893615 -3600
# Node ID 0c15caf47040b1bd29823cb155e811c0e72e8d45
# Parent  9ff441f295c23ee015a158783f016699f10daee6
clarified Keyword.is_keyword: union of minor and major;
misc tuning and simplification;

diff -r 9ff441f295c2 -r 0c15caf47040 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Mar 15 23:06:22 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Mar 16 11:26:55 2012 +0100
@@ -57,7 +57,7 @@
 val normalize_chained_theorems =
   maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
 fun reserved_isar_keyword_table () =
-  union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ())
+  Keyword.dest () |-> union (op =)
   |> map (rpair ()) |> Symtab.make
 
 end;
diff -r 9ff441f295c2 -r 0c15caf47040 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Thu Mar 15 23:06:22 2012 +0100
+++ b/src/Pure/Isar/keyword.ML	Fri Mar 16 11:26:55 2012 +0100
@@ -40,14 +40,11 @@
   val make: string * string list -> T
   val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
   val is_keyword: string -> bool
-  val dest_keywords: unit -> string list
-  val dest_commands: unit -> string list
   val command_keyword: string -> T option
   val command_tags: string -> string list
+  val dest: unit -> string list * string list
   val keyword_statusN: string
   val status: unit -> unit
-  val keyword: string -> unit
-  val command: string -> T -> unit
   val declare: string -> T option -> unit
   val is_diag: string -> bool
   val is_control: string -> bool
@@ -153,31 +150,45 @@
 
 (** global keyword tables **)
 
+type keywords =
+ {lexicons: Scan.lexicon * Scan.lexicon,  (*minor, major*)
+  commands: T Symtab.table};  (*command classification*)
+
+fun make_keywords (lexicons, commands) : keywords =
+  {lexicons = lexicons, commands = commands};
+
 local
 
-val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
-val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
+val global_keywords =
+  Unsynchronized.ref (make_keywords ((Scan.empty_lexicon, Scan.empty_lexicon), Symtab.empty));
 
 in
 
-fun get_commands () = ! global_commands;
-fun get_lexicons () = ! global_lexicons;
+fun get_keywords () = ! global_keywords;
 
-fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
-fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
+fun change_keywords f = CRITICAL (fn () =>
+  Unsynchronized.change global_keywords
+    (fn {lexicons, commands} => make_keywords (f (lexicons, commands))));
 
 end;
 
+fun get_lexicons () = #lexicons (get_keywords ());
+fun get_commands () = #commands (get_keywords ());
+
 
 (* lookup *)
 
-fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
-fun dest_keywords () = sort_strings (Scan.dest_lexicon (#1 (get_lexicons ())));
+fun is_keyword s =
+  let
+    val (minor, major) = get_lexicons ();
+    val syms = Symbol.explode s;
+  in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
 
-fun dest_commands () = sort_strings (Symtab.keys (get_commands ()));
 fun command_keyword name = Symtab.lookup (get_commands ()) name;
 fun command_tags name = these (Option.map tags_of (command_keyword name));
 
+fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());
+
 
 (* status *)
 
@@ -196,27 +207,28 @@
     ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")");
 
 fun status () =
-  let val (keywords, commands) = CRITICAL (fn () =>
-    (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
-  in
-    List.app keyword_status keywords;
-    List.app command_status commands
-  end;
+  let
+    val {lexicons = (minor, _), commands} = get_keywords ();
+    val _ = List.app keyword_status (sort_strings (Scan.dest_lexicon minor));
+    val _ = List.app command_status (sort_wrt #1 (Symtab.dest commands));
+  in () end;
 
 
-(* augment tables *)
-
-fun keyword name =
- (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
-  keyword_status name);
+(* declare *)
 
-fun command name kind =
- (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
-  change_commands (Symtab.update (name, kind));
-  command_status (name, kind));
-
-fun declare name NONE = keyword name
-  | declare name (SOME kind) = command name kind;
+fun declare name NONE =
+     (change_keywords (fn ((minor, major), commands) =>
+        let
+          val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
+        in ((minor', major), commands) end);
+      keyword_status name)
+  | declare name (SOME kind) =
+     (change_keywords (fn ((minor, major), commands) =>
+        let
+          val major' = Scan.extend_lexicon (Symbol.explode name) major;
+          val commands' = Symtab.update (name, kind) commands;
+        in ((minor, major'), commands') end);
+      command_status (name, kind));
 
 
 (* command categories *)
diff -r 9ff441f295c2 -r 0c15caf47040 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Mar 15 23:06:22 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 11:26:55 2012 +0100
@@ -131,9 +131,8 @@
           if k = SOME kind then ()
           else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
       | NONE =>
-          (Keyword.command name kind;
-           if Context.theory_name thy = Context.PureN then ()
-           else error ("Undeclared outer syntax command " ^ quote name)));
+          if Context.theory_name thy = Context.PureN then Keyword.declare name (SOME kind)
+          else error ("Undeclared outer syntax command " ^ quote name));
   in
     Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
      (if not (Symtab.defined commands name) then ()
@@ -178,8 +177,8 @@
 
 fun print_outer_syntax () =
   let
-    val (keywords, outer_syntax) =
-      CRITICAL (fn () => (Keyword.dest_keywords (), #2 (get_syntax ())));
+    val ((keywords, _), outer_syntax) =
+      CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
     fun pretty_cmd (name, comment, _) =
       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);
diff -r 9ff441f295c2 -r 0c15caf47040 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Mar 15 23:06:22 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Mar 16 11:26:55 2012 +0100
@@ -314,8 +314,7 @@
 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
 
 fun lexicalstructure_keywords () =
-    let val keywords = Keyword.dest_keywords ()
-        val commands = Keyword.dest_commands ()
+    let val (keywords, commands) = Keyword.dest ()
         fun keyword_elt kind keyword =
             XML.Elem (("keyword", [("word", keyword), ("category", kind)]), [])
         in
diff -r 9ff441f295c2 -r 0c15caf47040 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Mar 15 23:06:22 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML	Fri Mar 16 11:26:55 2012 +0100
@@ -626,7 +626,7 @@
 
 (* embedded lemma *)
 
-val _ = Keyword.keyword "by";
+val _ = Keyword.declare "by" NONE;  (*overlap with command category*)
 
 val _ =
   Context.>> (Context.map_theory