changeset 22214 | 6e9ab159512f |
parent 22130 | 0906fd95e0b5 |
child 22587 | 5454b06320fb |
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 |