# HG changeset patch
# User nipkow
# Date 1220257214 -7200
# Node ID 611e504c11914f34c983b1160bcde6da40708f2c
# Parent  3899dff63cd7e12ab6df964dc9bd10afb13fce6a
extended interface to preferences to allow adding new ones

diff -r 3899dff63cd7 -r 611e504c1191 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
diff -r 3899dff63cd7 -r 611e504c1191 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Sep 01 10:19:38 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Sep 01 10:20:14 2008 +0200
@@ -20,6 +20,7 @@
   val error_with_pos : PgipTypes.displayarea -> PgipTypes.fatality -> Position.T -> string -> unit
 
   val get_currently_open_file : unit -> Path.T option  (* interface focus *)
+  val add_preference: string -> Preferences.isa_preference -> unit
 end
 
 structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
@@ -339,6 +340,9 @@
 
 val preferences = ref Preferences.preferences;
 
+fun add_preference cat pref =
+    preferences := Preferences.add cat pref (!preferences);
+
 fun setup_preferences_tweak() =
     preferences :=
      (!preferences |> Preferences.set_default ("show-question-marks","false")