src/Pure/ProofGeneral/preferences.ML
changeset 22214 6e9ab159512f
parent 22130 0906fd95e0b5
child 22587 5454b06320fb
equal deleted inserted replaced
22213:2dd23002c465 22214:6e9ab159512f
    14 			  default: string,
    14 			  default: string,
    15 			  pgiptype: pgiptype,
    15 			  pgiptype: pgiptype,
    16 			  get: unit -> string,
    16 			  get: unit -> string,
    17 			  set: string -> unit }
    17 			  set: string -> unit }
    18 
    18 
    19   val preferences : (string * isa_preference list) list
    19   (* table of categorised and preferences; names must be unique *)
       
    20   type isa_preference_table = (string * isa_preference list) list
       
    21 
       
    22   val preferences : isa_preference_table
       
    23 
       
    24   val remove      : string -> isa_preference_table -> isa_preference_table
       
    25   val set_default : string * string -> isa_preference_table -> isa_preference_table
    20 end
    26 end
    21 
    27 
    22 structure Preferences : PREFERENCES =
    28 structure Preferences : PREFERENCES =
    23 struct
    29 struct
    24 
    30 
   149     [("Display", display_preferences),
   155     [("Display", display_preferences),
   150      ("Advanced Display", advanced_display_preferences),
   156      ("Advanced Display", advanced_display_preferences),
   151      ("Tracing", tracing_preferences),
   157      ("Tracing", tracing_preferences),
   152      ("Proof", proof_preferences)]
   158      ("Proof", proof_preferences)]
   153 
   159 
       
   160 type isa_preference_table = (string * isa_preference list) list
       
   161 
       
   162 fun remove name (preftable : isa_preference_table)  = 
       
   163     map (fn (cat,prefs) => 
       
   164 	    (cat, filter_out (curry op= name o #name) prefs))
       
   165         preftable;
       
   166 
       
   167 fun set_default (setname,newdefault) (preftable : isa_preference_table)  = 
       
   168     map (fn (cat,prefs) => 
       
   169 	    (cat, map (fn (pref as {name,descr,default,pgiptype,get,set})
       
   170 			  => if (name = setname) then 
       
   171 				 (set newdefault;
       
   172 				  {name=name,descr=descr,default=newdefault,
       
   173 				  pgiptype=pgiptype,get=get,set=set})
       
   174 			     else pref)
       
   175    		  prefs))
       
   176         preftable;
       
   177 
   154 end
   178 end