1.1 --- a/src/Pure/Isar/keyword.ML	Thu Mar 15 23:06:22 2012 +0100
     1.2 +++ b/src/Pure/Isar/keyword.ML	Fri Mar 16 11:26:55 2012 +0100
     1.3 @@ -40,14 +40,11 @@
     1.4    val make: string * string list -> T
     1.5    val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
     1.6    val is_keyword: string -> bool
     1.7 -  val dest_keywords: unit -> string list
     1.8 -  val dest_commands: unit -> string list
     1.9    val command_keyword: string -> T option
    1.10    val command_tags: string -> string list
    1.11 +  val dest: unit -> string list * string list
    1.12    val keyword_statusN: string
    1.13    val status: unit -> unit
    1.14 -  val keyword: string -> unit
    1.15 -  val command: string -> T -> unit
    1.16    val declare: string -> T option -> unit
    1.17    val is_diag: string -> bool
    1.18    val is_control: string -> bool
    1.19 @@ -153,31 +150,45 @@
    1.20  
    1.21  (** global keyword tables **)
    1.22  
    1.23 +type keywords =
    1.24 + {lexicons: Scan.lexicon * Scan.lexicon,  (*minor, major*)
    1.25 +  commands: T Symtab.table};  (*command classification*)
    1.26 +
    1.27 +fun make_keywords (lexicons, commands) : keywords =
    1.28 +  {lexicons = lexicons, commands = commands};
    1.29 +
    1.30  local
    1.31  
    1.32 -val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
    1.33 -val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
    1.34 +val global_keywords =
    1.35 +  Unsynchronized.ref (make_keywords ((Scan.empty_lexicon, Scan.empty_lexicon), Symtab.empty));
    1.36  
    1.37  in
    1.38  
    1.39 -fun get_commands () = ! global_commands;
    1.40 -fun get_lexicons () = ! global_lexicons;
    1.41 +fun get_keywords () = ! global_keywords;
    1.42  
    1.43 -fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
    1.44 -fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
    1.45 +fun change_keywords f = CRITICAL (fn () =>
    1.46 +  Unsynchronized.change global_keywords
    1.47 +    (fn {lexicons, commands} => make_keywords (f (lexicons, commands))));
    1.48  
    1.49  end;
    1.50  
    1.51 +fun get_lexicons () = #lexicons (get_keywords ());
    1.52 +fun get_commands () = #commands (get_keywords ());
    1.53 +
    1.54  
    1.55  (* lookup *)
    1.56  
    1.57 -fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
    1.58 -fun dest_keywords () = sort_strings (Scan.dest_lexicon (#1 (get_lexicons ())));
    1.59 +fun is_keyword s =
    1.60 +  let
    1.61 +    val (minor, major) = get_lexicons ();
    1.62 +    val syms = Symbol.explode s;
    1.63 +  in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
    1.64  
    1.65 -fun dest_commands () = sort_strings (Symtab.keys (get_commands ()));
    1.66  fun command_keyword name = Symtab.lookup (get_commands ()) name;
    1.67  fun command_tags name = these (Option.map tags_of (command_keyword name));
    1.68  
    1.69 +fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());
    1.70 +
    1.71  
    1.72  (* status *)
    1.73  
    1.74 @@ -196,27 +207,28 @@
    1.75      ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")");
    1.76  
    1.77  fun status () =
    1.78 -  let val (keywords, commands) = CRITICAL (fn () =>
    1.79 -    (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
    1.80 -  in
    1.81 -    List.app keyword_status keywords;
    1.82 -    List.app command_status commands
    1.83 -  end;
    1.84 +  let
    1.85 +    val {lexicons = (minor, _), commands} = get_keywords ();
    1.86 +    val _ = List.app keyword_status (sort_strings (Scan.dest_lexicon minor));
    1.87 +    val _ = List.app command_status (sort_wrt #1 (Symtab.dest commands));
    1.88 +  in () end;
    1.89  
    1.90  
    1.91 -(* augment tables *)
    1.92 +(* declare *)
    1.93  
    1.94 -fun keyword name =
    1.95 - (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
    1.96 -  keyword_status name);
    1.97 -
    1.98 -fun command name kind =
    1.99 - (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
   1.100 -  change_commands (Symtab.update (name, kind));
   1.101 -  command_status (name, kind));
   1.102 -
   1.103 -fun declare name NONE = keyword name
   1.104 -  | declare name (SOME kind) = command name kind;
   1.105 +fun declare name NONE =
   1.106 +     (change_keywords (fn ((minor, major), commands) =>
   1.107 +        let
   1.108 +          val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
   1.109 +        in ((minor', major), commands) end);
   1.110 +      keyword_status name)
   1.111 +  | declare name (SOME kind) =
   1.112 +     (change_keywords (fn ((minor, major), commands) =>
   1.113 +        let
   1.114 +          val major' = Scan.extend_lexicon (Symbol.explode name) major;
   1.115 +          val commands' = Symtab.update (name, kind) commands;
   1.116 +        in ((minor, major'), commands') end);
   1.117 +      command_status (name, kind));
   1.118  
   1.119  
   1.120  (* command categories *)