1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Mar 15 23:06:22 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Mar 16 11:26:55 2012 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4  val normalize_chained_theorems =
     1.5    maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
     1.6  fun reserved_isar_keyword_table () =
     1.7 -  union (op =) (Keyword.dest_keywords ()) (Keyword.dest_commands ())
     1.8 +  Keyword.dest () |-> union (op =)
     1.9    |> map (rpair ()) |> Symtab.make
    1.10  
    1.11  end;

     2.1 --- a/src/Pure/Isar/keyword.ML	Thu Mar 15 23:06:22 2012 +0100
     2.2 +++ b/src/Pure/Isar/keyword.ML	Fri Mar 16 11:26:55 2012 +0100
     2.3 @@ -40,14 +40,11 @@
     2.4    val make: string * string list -> T
     2.5    val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
     2.6    val is_keyword: string -> bool
     2.7 -  val dest_keywords: unit -> string list
     2.8 -  val dest_commands: unit -> string list
     2.9    val command_keyword: string -> T option
    2.10    val command_tags: string -> string list
    2.11 +  val dest: unit -> string list * string list
    2.12    val keyword_statusN: string
    2.13    val status: unit -> unit
    2.14 -  val keyword: string -> unit
    2.15 -  val command: string -> T -> unit
    2.16    val declare: string -> T option -> unit
    2.17    val is_diag: string -> bool
    2.18    val is_control: string -> bool
    2.19 @@ -153,31 +150,45 @@
    2.20  
    2.21  (** global keyword tables **)
    2.22  
    2.23 +type keywords =
    2.24 + {lexicons: Scan.lexicon * Scan.lexicon,  (*minor, major*)
    2.25 +  commands: T Symtab.table};  (*command classification*)
    2.26 +
    2.27 +fun make_keywords (lexicons, commands) : keywords =
    2.28 +  {lexicons = lexicons, commands = commands};
    2.29 +
    2.30  local
    2.31  
    2.32 -val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
    2.33 -val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
    2.34 +val global_keywords =
    2.35 +  Unsynchronized.ref (make_keywords ((Scan.empty_lexicon, Scan.empty_lexicon), Symtab.empty));
    2.36  
    2.37  in
    2.38  
    2.39 -fun get_commands () = ! global_commands;
    2.40 -fun get_lexicons () = ! global_lexicons;
    2.41 +fun get_keywords () = ! global_keywords;
    2.42  
    2.43 -fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
    2.44 -fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
    2.45 +fun change_keywords f = CRITICAL (fn () =>
    2.46 +  Unsynchronized.change global_keywords
    2.47 +    (fn {lexicons, commands} => make_keywords (f (lexicons, commands))));
    2.48  
    2.49  end;
    2.50  
    2.51 +fun get_lexicons () = #lexicons (get_keywords ());
    2.52 +fun get_commands () = #commands (get_keywords ());
    2.53 +
    2.54  
    2.55  (* lookup *)
    2.56  
    2.57 -fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
    2.58 -fun dest_keywords () = sort_strings (Scan.dest_lexicon (#1 (get_lexicons ())));
    2.59 +fun is_keyword s =
    2.60 +  let
    2.61 +    val (minor, major) = get_lexicons ();
    2.62 +    val syms = Symbol.explode s;
    2.63 +  in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
    2.64  
    2.65 -fun dest_commands () = sort_strings (Symtab.keys (get_commands ()));
    2.66  fun command_keyword name = Symtab.lookup (get_commands ()) name;
    2.67  fun command_tags name = these (Option.map tags_of (command_keyword name));
    2.68  
    2.69 +fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());
    2.70 +
    2.71  
    2.72  (* status *)
    2.73  
    2.74 @@ -196,27 +207,28 @@
    2.75      ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")");
    2.76  
    2.77  fun status () =
    2.78 -  let val (keywords, commands) = CRITICAL (fn () =>
    2.79 -    (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
    2.80 -  in
    2.81 -    List.app keyword_status keywords;
    2.82 -    List.app command_status commands
    2.83 -  end;
    2.84 +  let
    2.85 +    val {lexicons = (minor, _), commands} = get_keywords ();
    2.86 +    val _ = List.app keyword_status (sort_strings (Scan.dest_lexicon minor));
    2.87 +    val _ = List.app command_status (sort_wrt #1 (Symtab.dest commands));
    2.88 +  in () end;
    2.89  
    2.90  
    2.91 -(* augment tables *)
    2.92 +(* declare *)
    2.93  
    2.94 -fun keyword name =
    2.95 - (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
    2.96 -  keyword_status name);
    2.97 -
    2.98 -fun command name kind =
    2.99 - (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
   2.100 -  change_commands (Symtab.update (name, kind));
   2.101 -  command_status (name, kind));
   2.102 -
   2.103 -fun declare name NONE = keyword name
   2.104 -  | declare name (SOME kind) = command name kind;
   2.105 +fun declare name NONE =
   2.106 +     (change_keywords (fn ((minor, major), commands) =>
   2.107 +        let
   2.108 +          val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
   2.109 +        in ((minor', major), commands) end);
   2.110 +      keyword_status name)
   2.111 +  | declare name (SOME kind) =
   2.112 +     (change_keywords (fn ((minor, major), commands) =>
   2.113 +        let
   2.114 +          val major' = Scan.extend_lexicon (Symbol.explode name) major;
   2.115 +          val commands' = Symtab.update (name, kind) commands;
   2.116 +        in ((minor, major'), commands') end);
   2.117 +      command_status (name, kind));
   2.118  
   2.119  
   2.120  (* command categories *)

     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Mar 15 23:06:22 2012 +0100
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 11:26:55 2012 +0100
     3.3 @@ -131,9 +131,8 @@
     3.4            if k = SOME kind then ()
     3.5            else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
     3.6        | NONE =>
     3.7 -          (Keyword.command name kind;
     3.8 -           if Context.theory_name thy = Context.PureN then ()
     3.9 -           else error ("Undeclared outer syntax command " ^ quote name)));
    3.10 +          if Context.theory_name thy = Context.PureN then Keyword.declare name (SOME kind)
    3.11 +          else error ("Undeclared outer syntax command " ^ quote name));
    3.12    in
    3.13      Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
    3.14       (if not (Symtab.defined commands name) then ()
    3.15 @@ -178,8 +177,8 @@
    3.16  
    3.17  fun print_outer_syntax () =
    3.18    let
    3.19 -    val (keywords, outer_syntax) =
    3.20 -      CRITICAL (fn () => (Keyword.dest_keywords (), #2 (get_syntax ())));
    3.21 +    val ((keywords, _), outer_syntax) =
    3.22 +      CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
    3.23      fun pretty_cmd (name, comment, _) =
    3.24        Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    3.25      val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax);

     4.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Mar 15 23:06:22 2012 +0100
     4.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Mar 16 11:26:55 2012 +0100
     4.3 @@ -314,8 +314,7 @@
     4.4  (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
     4.5  
     4.6  fun lexicalstructure_keywords () =
     4.7 -    let val keywords = Keyword.dest_keywords ()
     4.8 -        val commands = Keyword.dest_commands ()
     4.9 +    let val (keywords, commands) = Keyword.dest ()
    4.10          fun keyword_elt kind keyword =
    4.11              XML.Elem (("keyword", [("word", keyword), ("category", kind)]), [])
    4.12          in

     5.1 --- a/src/Pure/Thy/thy_output.ML	Thu Mar 15 23:06:22 2012 +0100
     5.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Mar 16 11:26:55 2012 +0100
     5.3 @@ -626,7 +626,7 @@
     5.4  
     5.5  (* embedded lemma *)
     5.6  
     5.7 -val _ = Keyword.keyword "by";
     5.8 +val _ = Keyword.declare "by" NONE;  (*overlap with command category*)
     5.9  
    5.10  val _ =
    5.11    Context.>> (Context.map_theory