5 User preferences for Isabelle which are maintained by the interface. |
5 User preferences for Isabelle which are maintained by the interface. |
6 *) |
6 *) |
7 |
7 |
8 signature PREFERENCES = |
8 signature PREFERENCES = |
9 sig |
9 sig |
10 type pgiptype = PgipTypes.pgiptype |
10 type preference = |
11 |
11 {name: string, |
12 type isa_preference = { name: string, |
12 descr: string, |
13 descr: string, |
13 default: string, |
14 default: string, |
14 pgiptype: PgipTypes.pgiptype, |
15 pgiptype: pgiptype, |
15 get: unit -> string, |
16 get: unit -> string, |
16 set: string -> unit} |
17 set: string -> unit } |
17 val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype -> |
18 |
18 'a ref -> string -> string -> preference |
19 (* table of categories and preferences; names must be unique *) |
19 val string_pref: string ref -> string -> string -> preference |
20 type isa_preference_table = (string * isa_preference list) list |
20 val int_pref: int ref -> string -> string -> preference |
21 |
21 val nat_pref: int ref -> string -> string -> preference |
22 val preferences : isa_preference_table |
22 val bool_pref: bool ref -> string -> string -> preference |
23 |
23 type T = (string * preference list) list |
24 val remove : string -> isa_preference_table -> isa_preference_table |
24 val pure_preferences: T |
25 val add : string -> isa_preference |
25 val remove: string -> T -> T |
26 -> isa_preference_table -> isa_preference_table |
26 val add: string -> preference -> T -> T |
27 val set_default : string * string -> isa_preference_table -> isa_preference_table |
27 val set_default: string * string -> T -> T |
28 end |
28 end |
29 |
29 |
30 structure Preferences : PREFERENCES = |
30 structure Preferences: PREFERENCES = |
31 struct |
31 struct |
32 |
32 |
33 val thm_depsN = "thm_deps"; (* also in proof_general_pgip.ML: move to pgip_isabelle? *) |
33 (* preferences and preference tables *) |
34 |
34 |
35 type pgiptype = PgipTypes.pgiptype |
35 type preference = |
36 |
36 {name: string, |
37 type isa_preference = { name: string, |
37 descr: string, |
38 descr: string, |
38 default: string, |
39 default: string, |
39 pgiptype: PgipTypes.pgiptype, |
40 pgiptype: pgiptype, |
40 get: unit -> string, |
41 get: unit -> string, |
41 set: string -> unit}; |
42 set: string -> unit } |
42 |
43 |
43 fun mkpref raw_get raw_set typ name descr : preference = |
44 |
44 let |
45 fun mkpref get set typ nm descr = |
45 fun get () = CRITICAL raw_get; |
46 { name=nm, descr=descr, pgiptype=typ, get=get, set=set, default=get() } : isa_preference |
46 fun set x = CRITICAL (fn () => raw_set x); |
47 |
47 in {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()} end; |
48 fun mkpref_from_ref read write typ r nm descr = |
48 |
49 mkpref (fn()=> read (!r)) (fn v=> r:= (write v)) typ nm descr |
49 |
|
50 (* generic preferences *) |
|
51 |
|
52 fun generic_pref read write typ r = |
|
53 mkpref (fn () => read (! r)) (fn x => r := write x) typ; |
|
54 |
|
55 val string_pref = generic_pref I I PgipTypes.Pgipstring; |
50 |
56 |
51 val int_pref = |
57 val int_pref = |
52 mkpref_from_ref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE,NONE)) |
58 generic_pref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE, NONE)) |
53 (PgipTypes.Pgipint (NONE, NONE)) |
59 (PgipTypes.Pgipint (NONE, NONE)); |
|
60 |
54 val nat_pref = |
61 val nat_pref = |
55 mkpref_from_ref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat |
62 generic_pref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat; |
56 |
63 |
57 val bool_pref = |
64 val bool_pref = |
58 mkpref_from_ref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool |
65 generic_pref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool; |
|
66 |
|
67 |
|
68 (* preferences of Pure *) |
59 |
69 |
60 val proof_pref = |
70 val proof_pref = |
61 let |
71 let |
62 fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2) |
72 fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2); |
63 fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1) |
73 fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1); |
64 in |
74 in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end; |
65 mkpref get set PgipTypes.Pgipbool "full-proofs" |
75 |
66 "Record full proof objects internally" |
76 val thm_depsN = "thm_deps"; |
67 end |
|
68 |
|
69 val thm_deps_pref = |
77 val thm_deps_pref = |
70 let |
78 let |
71 fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN) |
79 fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN); |
72 fun set s = NAMED_CRITICAL "print_mode" (fn () => |
80 fun set s = |
73 if PgipTypes.read_pgipbool s then |
81 if PgipTypes.read_pgipbool s then change print_mode (insert (op =) thm_depsN) |
74 change print_mode (insert (op =) thm_depsN) |
82 else change print_mode (remove (op =) thm_depsN); |
75 else |
83 in |
76 change print_mode (remove (op =) thm_depsN)) |
84 mkpref get set PgipTypes.Pgipbool "theorem-dependencies" |
77 in |
85 "Track theorem dependencies within Proof General" |
78 mkpref get set PgipTypes.Pgipbool "theorem-dependencies" |
86 end; |
79 "Track theorem dependencies within Proof General" |
|
80 end |
|
81 |
87 |
82 val print_depth_pref = |
88 val print_depth_pref = |
83 let |
89 let |
84 fun get () = PgipTypes.int_to_pgstring (get_print_depth ()) |
90 fun get () = PgipTypes.int_to_pgstring (get_print_depth ()); |
85 val set = print_depth o PgipTypes.read_pgipnat |
91 val set = print_depth o PgipTypes.read_pgipnat; |
86 in |
92 in mkpref get set PgipTypes.Pgipnat "print-depth" "Setting for the ML print depth" end; |
87 mkpref get set PgipTypes.Pgipnat |
|
88 "print-depth" "Setting for the ML print depth" |
|
89 end |
|
90 |
93 |
91 |
94 |
92 val display_preferences = |
95 val display_preferences = |
93 [bool_pref show_types |
96 [bool_pref show_types |
94 "show-types" |
97 "show-types" |
95 "Include types in display of Isabelle terms", |
98 "Include types in display of Isabelle terms", |
96 bool_pref show_sorts |
99 bool_pref show_sorts |
97 "show-sorts" |
100 "show-sorts" |
98 "Include sorts in display of Isabelle terms", |
101 "Include sorts in display of Isabelle terms", |
99 bool_pref show_consts |
102 bool_pref show_consts |
100 "show-consts" |
103 "show-consts" |
101 "Show types of consts in Isabelle goal display", |
104 "Show types of consts in Isabelle goal display", |
102 bool_pref long_names |
105 bool_pref long_names |
103 "long-names" |
106 "long-names" |
104 "Show fully qualified names in Isabelle terms", |
107 "Show fully qualified names in Isabelle terms", |
105 bool_pref show_brackets |
108 bool_pref show_brackets |
106 "show-brackets" |
109 "show-brackets" |
107 "Show full bracketing in Isabelle terms", |
110 "Show full bracketing in Isabelle terms", |
108 bool_pref Proof.show_main_goal |
111 bool_pref Proof.show_main_goal |
109 "show-main-goal" |
112 "show-main-goal" |
110 "Show main goal in proof state display", |
113 "Show main goal in proof state display", |
111 bool_pref Syntax.eta_contract |
114 bool_pref Syntax.eta_contract |
112 "eta-contract" |
115 "eta-contract" |
113 "Print terms eta-contracted"] |
116 "Print terms eta-contracted"]; |
114 |
117 |
115 val advanced_display_preferences = |
118 val advanced_display_preferences = |
116 [nat_pref goals_limit |
119 [nat_pref goals_limit |
117 "goals-limit" |
120 "goals-limit" |
118 "Setting for maximum number of goals printed", |
121 "Setting for maximum number of goals printed", |
119 int_pref ProofContext.prems_limit |
122 int_pref ProofContext.prems_limit |
120 "prems-limit" |
123 "prems-limit" |
121 "Setting for maximum number of premises printed", |
124 "Setting for maximum number of premises printed", |
122 print_depth_pref, |
125 print_depth_pref, |
123 bool_pref show_question_marks |
126 bool_pref show_question_marks |
124 "show-question-marks" |
127 "show-question-marks" |
125 "Show leading question mark of variable name"] |
128 "Show leading question mark of variable name"]; |
126 |
129 |
127 val tracing_preferences = |
130 val tracing_preferences = |
128 [bool_pref trace_simp |
131 [bool_pref trace_simp |
129 "trace-simplifier" |
132 "trace-simplifier" |
130 "Trace simplification rules.", |
133 "Trace simplification rules.", |
131 nat_pref trace_simp_depth_limit |
134 nat_pref trace_simp_depth_limit |
132 "trace-simplifier-depth" |
135 "trace-simplifier-depth" |
133 "Trace simplifier depth limit.", |
136 "Trace simplifier depth limit.", |
134 bool_pref trace_rules |
137 bool_pref trace_rules |
135 "trace-rules" |
138 "trace-rules" |
136 "Trace application of the standard rules", |
139 "Trace application of the standard rules", |
137 bool_pref Pattern.trace_unify_fail |
140 bool_pref Pattern.trace_unify_fail |
138 "trace-unification" |
141 "trace-unification" |
139 "Output error diagnostics during unification", |
142 "Output error diagnostics during unification", |
140 bool_pref Output.timing |
143 bool_pref Output.timing |
141 "global-timing" |
144 "global-timing" |
142 "Whether to enable timing in Isabelle.", |
145 "Whether to enable timing in Isabelle.", |
143 bool_pref Toplevel.debug |
146 bool_pref Toplevel.debug |
144 "debugging" |
147 "debugging" |
145 "Whether to enable debugging.", |
148 "Whether to enable debugging.", |
146 bool_pref Quickcheck.auto |
149 bool_pref Quickcheck.auto |
147 "auto-quickcheck" |
150 "auto-quickcheck" |
148 "Whether to enable quickcheck automatically.", |
151 "Whether to enable quickcheck automatically.", |
149 nat_pref Quickcheck.auto_time_limit |
152 nat_pref Quickcheck.auto_time_limit |
150 "auto-quickcheck-time-limit" |
153 "auto-quickcheck-time-limit" |
151 "Time limit for automatic quickcheck (in milliseconds).", |
154 "Time limit for automatic quickcheck (in milliseconds).", |
152 thm_deps_pref] |
155 thm_deps_pref]; |
153 |
156 |
154 val proof_preferences = |
157 val proof_preferences = |
155 [bool_pref quick_and_dirty |
158 [bool_pref quick_and_dirty |
156 "quick-and-dirty" |
159 "quick-and-dirty" |
157 "Take a few short cuts", |
160 "Take a few short cuts", |
158 bool_pref Toplevel.skip_proofs |
161 bool_pref Toplevel.skip_proofs |
159 "skip-proofs" |
162 "skip-proofs" |
160 "Skip over proofs (interactive-only)", |
163 "Skip over proofs (interactive-only)", |
161 proof_pref, |
164 proof_pref, |
162 nat_pref Multithreading.max_threads |
165 nat_pref Multithreading.max_threads |
163 "max-threads" |
166 "max-threads" |
164 "Maximum number of threads"] |
167 "Maximum number of threads"]; |
165 |
168 |
166 val preferences = |
169 val pure_preferences = |
167 [("Display", display_preferences), |
170 [("Display", display_preferences), |
168 ("Advanced Display", advanced_display_preferences), |
171 ("Advanced Display", advanced_display_preferences), |
169 ("Tracing", tracing_preferences), |
172 ("Tracing", tracing_preferences), |
170 ("Proof", proof_preferences)] |
173 ("Proof", proof_preferences)]; |
171 |
174 |
172 type isa_preference_table = (string * isa_preference list) list |
175 |
173 |
176 (* table of categories and preferences; names must be unique *) |
174 fun remove name (preftable : isa_preference_table) = |
177 |
175 map (fn (cat,prefs) => |
178 type T = (string * preference list) list; |
176 (cat, filter_out (curry op= name o #name) prefs)) |
179 |
177 preftable; |
180 fun remove name (tab: T) = tab |> map |
178 |
181 (fn (cat, prefs) => (cat, filter_out (curry op = name o #name) prefs)); |
179 fun set_default (setname,newdefault) (preftable : isa_preference_table) = |
182 |
180 map (fn (cat,prefs) => |
183 fun set_default (setname, newdefault) (tab: T) = tab |> map |
181 (cat, map (fn (pref as {name,descr,default,pgiptype,get,set}) |
184 (fn (cat, prefs) => |
182 => if (name = setname) then |
185 (cat, prefs |> map (fn (pref as {name, descr, default, pgiptype, get, set}) => |
183 (set newdefault; |
186 if name = setname then |
184 {name=name,descr=descr,default=newdefault, |
187 (set newdefault; |
185 pgiptype=pgiptype,get=get,set=set}) |
188 {name =name , descr = descr, default = newdefault, |
186 else pref) |
189 pgiptype = pgiptype, get = get, set = set}) |
187 prefs)) |
190 else pref))); |
188 preftable; |
191 |
189 |
192 fun add cname (pref: preference) (tab: T) = tab |> map |
190 fun add cname (pref: isa_preference) (preftable : isa_preference_table) = |
193 (fn (cat, prefs) => |
191 map (fn (cat,prefs:isa_preference list) => |
194 if cat <> cname then (cat, prefs) |
192 if cat <> cname then (cat,prefs) |
195 else |
193 else if (#name pref) mem (map #name prefs) |
196 if exists (fn {name, ...} => name = #name pref) prefs |
194 then error ("Preference already exists: " ^ quote(#name pref)) |
197 then error ("Preference already exists: " ^ quote (#name pref)) |
195 else (cat, pref::prefs)) preftable; |
198 else (cat, pref :: prefs)); |
196 |
199 |
197 end |
200 end; |