src/Pure/ProofGeneral/preferences.ML

--- a/src/Pure/ProofGeneral/preferences.ML	Mon Sep 01 10:19:38 2008 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Mon Sep 01 10:20:14 2008 +0200
@@ -22,6 +22,8 @@
   val preferences : isa_preference_table
 
   val remove      : string -> isa_preference_table -> isa_preference_table
+  val add         : string -> isa_preference
+                    -> isa_preference_table -> isa_preference_table
   val set_default : string * string -> isa_preference_table -> isa_preference_table
 end
 
@@ -185,4 +187,11 @@
                   prefs))
         preftable;
 
+fun add cname (pref: isa_preference) (preftable : isa_preference_table) =
+    map (fn (cat,prefs:isa_preference list) =>
+      if cat <> cname then (cat,prefs)
+      else if (#name pref) mem (map #name prefs)
+           then error ("Preference already exists: " ^ quote(#name pref))
+           else (cat, pref::prefs))  preftable;
+
 end