author | wenzelm |
Mon, 13 May 2013 22:00:19 +0200 | |
changeset 51970 | f08366cb9fd1 |
parent 51960 | 61ac1efe02c3 |
child 51971 | 716bb7e2e272 |
permissions | -rw-r--r-- |
21637 | 1 |
(* Title: Pure/ProofGeneral/preferences.ML |
2 |
Author: David Aspinall and Markus Wenzel |
|
3 |
||
4 |
User preferences for Isabelle which are maintained by the interface. |
|
5 |
*) |
|
6 |
||
24329 | 7 |
signature PREFERENCES = |
21637 | 8 |
sig |
30980 | 9 |
val category_display: string |
10 |
val category_advanced_display: string |
|
11 |
val category_tracing: string |
|
12 |
val category_proof: string |
|
28587 | 13 |
type preference = |
14 |
{name: string, |
|
15 |
descr: string, |
|
16 |
default: string, |
|
17 |
pgiptype: PgipTypes.pgiptype, |
|
18 |
get: unit -> string, |
|
19 |
set: string -> unit} |
|
51944 | 20 |
val options_pref: string -> string -> string -> preference |
28587 | 21 |
val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype -> |
32738 | 22 |
'a Unsynchronized.ref -> string -> string -> preference |
23 |
val string_pref: string Unsynchronized.ref -> string -> string -> preference |
|
40292 | 24 |
val real_pref: real Unsynchronized.ref -> string -> string -> preference |
32738 | 25 |
val int_pref: int Unsynchronized.ref -> string -> string -> preference |
26 |
val nat_pref: int Unsynchronized.ref -> string -> string -> preference |
|
27 |
val bool_pref: bool Unsynchronized.ref -> string -> string -> preference |
|
28587 | 28 |
type T = (string * preference list) list |
51970 | 29 |
val thm_depsN: string |
28587 | 30 |
val pure_preferences: T |
31 |
val remove: string -> T -> T |
|
32 |
val add: string -> preference -> T -> T |
|
33 |
val set_default: string * string -> T -> T |
|
21637 | 34 |
end |
35 |
||
28587 | 36 |
structure Preferences: PREFERENCES = |
21637 | 37 |
struct |
38 |
||
30980 | 39 |
(* categories *) |
40 |
||
41 |
val category_display = "Display"; |
|
42 |
val category_advanced_display = "Advanced Display"; |
|
43 |
val category_tracing = "Tracing"; |
|
44 |
val category_proof = "Proof" |
|
45 |
||
46 |
||
28587 | 47 |
(* preferences and preference tables *) |
21637 | 48 |
|
28587 | 49 |
type preference = |
50 |
{name: string, |
|
51 |
descr: string, |
|
52 |
default: string, |
|
53 |
pgiptype: PgipTypes.pgiptype, |
|
54 |
get: unit -> string, |
|
55 |
set: string -> unit}; |
|
56 |
||
51944 | 57 |
|
58 |
(* options as preferences *) |
|
59 |
||
60 |
fun options_pref option_name pgip_name descr : preference = |
|
61 |
let |
|
51946 | 62 |
val typ = Options.default_typ option_name; |
51944 | 63 |
val pgiptype = |
64 |
if typ = Options.boolT then PgipTypes.Pgipbool |
|
65 |
else if typ = Options.intT then PgipTypes.Pgipint (NONE, NONE) |
|
66 |
else if typ = Options.realT then PgipTypes.Pgipreal |
|
67 |
else PgipTypes.Pgipstring; |
|
68 |
in |
|
69 |
{name = pgip_name, |
|
70 |
descr = descr, |
|
71 |
default = Options.get_default option_name, |
|
72 |
pgiptype = pgiptype, |
|
73 |
get = fn () => Options.get_default option_name, |
|
74 |
set = Options.put_default option_name} |
|
75 |
end; |
|
76 |
||
77 |
||
78 |
(* generic preferences *) |
|
79 |
||
28587 | 80 |
fun mkpref raw_get raw_set typ name descr : preference = |
81 |
let |
|
82 |
fun get () = CRITICAL raw_get; |
|
83 |
fun set x = CRITICAL (fn () => raw_set x); |
|
84 |
in {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()} end; |
|
21637 | 85 |
|
28587 | 86 |
fun generic_pref read write typ r = |
87 |
mkpref (fn () => read (! r)) (fn x => r := write x) typ; |
|
88 |
||
89 |
val string_pref = generic_pref I I PgipTypes.Pgipstring; |
|
21637 | 90 |
|
40292 | 91 |
val real_pref = |
92 |
generic_pref PgipTypes.real_to_pgstring PgipTypes.read_pgipreal PgipTypes.Pgipreal; |
|
93 |
||
24329 | 94 |
val int_pref = |
28587 | 95 |
generic_pref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE, NONE)) |
96 |
(PgipTypes.Pgipint (NONE, NONE)); |
|
97 |
||
21637 | 98 |
val nat_pref = |
28587 | 99 |
generic_pref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat; |
21637 | 100 |
|
101 |
val bool_pref = |
|
28587 | 102 |
generic_pref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool; |
103 |
||
104 |
||
105 |
(* preferences of Pure *) |
|
21637 | 106 |
|
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39165
diff
changeset
|
107 |
val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () => |
28587 | 108 |
let |
41698 | 109 |
fun get () = PgipTypes.bool_to_pgstring (Proofterm.proofs_enabled ()); |
28587 | 110 |
fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1); |
30980 | 111 |
in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) (); |
21637 | 112 |
|
32061
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset
|
113 |
val parallel_proof_pref = |
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset
|
114 |
let |
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset
|
115 |
fun get () = PgipTypes.bool_to_pgstring (! Goal.parallel_proofs >= 1); |
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset
|
116 |
fun set s = Goal.parallel_proofs := (if PgipTypes.read_pgipbool s then 1 else 0); |
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset
|
117 |
in mkpref get set PgipTypes.Pgipbool "parallel-proofs" "Check proofs in parallel" end; |
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset
|
118 |
|
28587 | 119 |
val thm_depsN = "thm_deps"; |
24329 | 120 |
val thm_deps_pref = |
28587 | 121 |
let |
122 |
fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN); |
|
123 |
fun set s = |
|
32738 | 124 |
if PgipTypes.read_pgipbool s |
125 |
then Unsynchronized.change print_mode (insert (op =) thm_depsN) |
|
126 |
else Unsynchronized.change print_mode (remove (op =) thm_depsN); |
|
28587 | 127 |
in |
128 |
mkpref get set PgipTypes.Pgipbool "theorem-dependencies" |
|
129 |
"Track theorem dependencies within Proof General" |
|
130 |
end; |
|
21637 | 131 |
|
132 |
val print_depth_pref = |
|
28587 | 133 |
let |
134 |
fun get () = PgipTypes.int_to_pgstring (get_print_depth ()); |
|
135 |
val set = print_depth o PgipTypes.read_pgipnat; |
|
136 |
in mkpref get set PgipTypes.Pgipnat "print-depth" "Setting for the ML print depth" end; |
|
21637 | 137 |
|
138 |
||
24329 | 139 |
val display_preferences = |
42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
140 |
[bool_pref Printer.show_types_default |
28587 | 141 |
"show-types" |
142 |
"Include types in display of Isabelle terms", |
|
42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
143 |
bool_pref Printer.show_sorts_default |
28587 | 144 |
"show-sorts" |
145 |
"Include sorts in display of Isabelle terms", |
|
42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
146 |
bool_pref Goal_Display.show_consts_default |
28587 | 147 |
"show-consts" |
148 |
"Show types of consts in Isabelle goal display", |
|
51949
f6858bb224c9
some system options as context-sensitive config options;
wenzelm
parents:
51946
diff
changeset
|
149 |
options_pref "names_long" |
28587 | 150 |
"long-names" |
151 |
"Show fully qualified names in Isabelle terms", |
|
42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
152 |
bool_pref Printer.show_brackets_default |
28587 | 153 |
"show-brackets" |
154 |
"Show full bracketing in Isabelle terms", |
|
39125
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39050
diff
changeset
|
155 |
bool_pref Goal_Display.show_main_goal_default |
28587 | 156 |
"show-main-goal" |
157 |
"Show main goal in proof state display", |
|
42284 | 158 |
bool_pref Syntax_Trans.eta_contract_default |
28587 | 159 |
"eta-contract" |
160 |
"Print terms eta-contracted"]; |
|
21637 | 161 |
|
162 |
val advanced_display_preferences = |
|
51960
61ac1efe02c3
option "goals_limit", with more uniform description;
wenzelm
parents:
51949
diff
changeset
|
163 |
[options_pref "goals_limit" |
28587 | 164 |
"goals-limit" |
51960
61ac1efe02c3
option "goals_limit", with more uniform description;
wenzelm
parents:
51949
diff
changeset
|
165 |
"Setting for maximum number of subgoals to be printed", |
28587 | 166 |
print_depth_pref, |
51949
f6858bb224c9
some system options as context-sensitive config options;
wenzelm
parents:
51946
diff
changeset
|
167 |
options_pref "show_question_marks" |
28587 | 168 |
"show-question-marks" |
169 |
"Show leading question mark of variable name"]; |
|
21637 | 170 |
|
24329 | 171 |
val tracing_preferences = |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41227
diff
changeset
|
172 |
[bool_pref Raw_Simplifier.simp_trace_default |
35995
26e820d27e0a
re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
boehmes
parents:
35979
diff
changeset
|
173 |
"trace-simplifier" |
26e820d27e0a
re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
boehmes
parents:
35979
diff
changeset
|
174 |
"Trace simplification rules.", |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41227
diff
changeset
|
175 |
nat_pref Raw_Simplifier.simp_trace_depth_limit_default |
28587 | 176 |
"trace-simplifier-depth" |
177 |
"Trace simplifier depth limit.", |
|
178 |
bool_pref Pattern.trace_unify_fail |
|
179 |
"trace-unification" |
|
180 |
"Output error diagnostics during unification", |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41698
diff
changeset
|
181 |
bool_pref Toplevel.timing |
28587 | 182 |
"global-timing" |
183 |
"Whether to enable timing in Isabelle.", |
|
184 |
bool_pref Toplevel.debug |
|
185 |
"debugging" |
|
186 |
"Whether to enable debugging.", |
|
187 |
thm_deps_pref]; |
|
21637 | 188 |
|
24329 | 189 |
val proof_preferences = |
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39165
diff
changeset
|
190 |
[Unsynchronized.setmp quick_and_dirty true (fn () => |
30980 | 191 |
bool_pref quick_and_dirty |
192 |
"quick-and-dirty" |
|
193 |
"Take a few short cuts") (), |
|
51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
48634
diff
changeset
|
194 |
bool_pref Goal.skip_proofs |
28587 | 195 |
"skip-proofs" |
48634 | 196 |
"Skip over proofs", |
28587 | 197 |
proof_pref, |
198 |
nat_pref Multithreading.max_threads |
|
199 |
"max-threads" |
|
29435
a5f84ac14609
added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
wenzelm
parents:
28591
diff
changeset
|
200 |
"Maximum number of threads", |
32061
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset
|
201 |
parallel_proof_pref]; |
21637 | 202 |
|
28587 | 203 |
val pure_preferences = |
30980 | 204 |
[(category_display, display_preferences), |
205 |
(category_advanced_display, advanced_display_preferences), |
|
206 |
(category_tracing, tracing_preferences), |
|
207 |
(category_proof, proof_preferences)]; |
|
21637 | 208 |
|
28587 | 209 |
|
210 |
(* table of categories and preferences; names must be unique *) |
|
211 |
||
212 |
type T = (string * preference list) list; |
|
22214
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset
|
213 |
|
28587 | 214 |
fun remove name (tab: T) = tab |> map |
215 |
(fn (cat, prefs) => (cat, filter_out (curry op = name o #name) prefs)); |
|
22214
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset
|
216 |
|
28587 | 217 |
fun set_default (setname, newdefault) (tab: T) = tab |> map |
218 |
(fn (cat, prefs) => |
|
219 |
(cat, prefs |> map (fn (pref as {name, descr, default, pgiptype, get, set}) => |
|
220 |
if name = setname then |
|
221 |
(set newdefault; |
|
222 |
{name =name , descr = descr, default = newdefault, |
|
223 |
pgiptype = pgiptype, get = get, set = set}) |
|
224 |
else pref))); |
|
22214
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset
|
225 |
|
28587 | 226 |
fun add cname (pref: preference) (tab: T) = tab |> map |
227 |
(fn (cat, prefs) => |
|
228 |
if cat <> cname then (cat, prefs) |
|
229 |
else |
|
230 |
if exists (fn {name, ...} => name = #name pref) prefs |
|
28591 | 231 |
then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs)) |
30985 | 232 |
else (cat, prefs @ [pref])); |
28066
611e504c1191
extended interface to preferences to allow adding new ones
nipkow
parents:
25440
diff
changeset
|
233 |
|
28587 | 234 |
end; |