# HG changeset patch
# User wenzelm
# Date 1345718692 -7200
# Node ID e54cf66928e67c7944e4a2ae3cbe7457caecc54d
# Parent  92da8a8380daf2922d22d26a2ec211b319222000
tuned signature (again, cf. ff9cd47be39b);

diff -r 92da8a8380da -r e54cf66928e6 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Thu Aug 23 12:43:01 2012 +0200
+++ b/src/Pure/Isar/keyword.ML	Thu Aug 23 12:44:52 2012 +0200
@@ -47,9 +47,6 @@
   type spec = (string * string list) * string list
   val spec: spec -> T
   val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
-  type keywords
-  val lexicons_of: keywords -> Scan.lexicon * Scan.lexicon
-  val get_keywords: unit -> keywords
   val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
   val is_keyword: string -> bool
   val command_keyword: string -> T option
@@ -57,7 +54,6 @@
   val command_tags: string -> string list
   val dest: unit -> string list * string list
   val status: unit -> unit
-  val define_keywords: string * T option -> keywords -> keywords
   val define: string * T option -> unit
   val is_diag: string -> bool
   val is_control: string -> bool
@@ -171,11 +167,6 @@
 fun make_keywords (lexicons, commands) =
   Keywords {lexicons = lexicons, commands = commands};
 
-fun map_keywords f (Keywords {lexicons, commands}) =
-  make_keywords (f (lexicons, commands));
-
-fun lexicons_of (Keywords {lexicons, ...}) = lexicons;
-
 local
 
 val global_keywords =
@@ -185,11 +176,13 @@
 
 fun get_keywords () = ! global_keywords;
 
-fun change_keywords f = CRITICAL (fn () => Unsynchronized.change global_keywords f);
+fun change_keywords f = CRITICAL (fn () =>
+  Unsynchronized.change global_keywords
+    (fn Keywords {lexicons, commands} => make_keywords (f (lexicons, commands))));
 
 end;
 
-fun get_lexicons () = lexicons_of (get_keywords ());
+fun get_lexicons () = get_keywords () |> (fn Keywords {lexicons, ...} => lexicons);
 fun get_commands () = get_keywords () |> (fn Keywords {commands, ...} => commands);
 
 
@@ -222,7 +215,7 @@
 
 (* define *)
 
-fun define_keywords (name, opt_kind) = map_keywords (fn ((minor, major), commands) =>
+fun define (name, opt_kind) = change_keywords (fn ((minor, major), commands) =>
   (case opt_kind of
     NONE =>
       let
@@ -234,8 +227,6 @@
         val commands' = Symtab.update (name, kind) commands;
       in ((minor, major'), commands') end));
 
-val define = change_keywords o define_keywords;
-
 
 (* command categories *)