author | wenzelm |
Tue, 14 May 2013 21:40:25 +0200 | |
changeset 51992 | 5c179451c445 |
parent 51991 | 5b814dd90f7f |
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, |
|
51992 | 17 |
pgiptype: string, |
28587 | 18 |
get: unit -> string, |
19 |
set: string -> unit} |
|
51944 | 20 |
val options_pref: string -> string -> string -> preference |
32738 | 21 |
val string_pref: string Unsynchronized.ref -> string -> string -> preference |
40292 | 22 |
val real_pref: real Unsynchronized.ref -> string -> string -> preference |
32738 | 23 |
val int_pref: int Unsynchronized.ref -> string -> string -> preference |
24 |
val bool_pref: bool Unsynchronized.ref -> string -> string -> preference |
|
28587 | 25 |
type T = (string * preference list) list |
51970 | 26 |
val thm_depsN: string |
28587 | 27 |
val pure_preferences: T |
28 |
val add: string -> preference -> T -> T |
|
21637 | 29 |
end |
30 |
||
28587 | 31 |
structure Preferences: PREFERENCES = |
21637 | 32 |
struct |
33 |
||
30980 | 34 |
(* categories *) |
35 |
||
36 |
val category_display = "Display"; |
|
37 |
val category_advanced_display = "Advanced Display"; |
|
38 |
val category_tracing = "Tracing"; |
|
39 |
val category_proof = "Proof" |
|
40 |
||
41 |
||
28587 | 42 |
(* preferences and preference tables *) |
21637 | 43 |
|
28587 | 44 |
type preference = |
45 |
{name: string, |
|
46 |
descr: string, |
|
47 |
default: string, |
|
51992 | 48 |
pgiptype: string, |
28587 | 49 |
get: unit -> string, |
50 |
set: string -> unit}; |
|
51 |
||
51992 | 52 |
val pgipbool = "pgipbool"; |
53 |
val pgipint = "pgipint"; |
|
54 |
val pgipfloat = "pgipint"; (*NB: PG 3.7.x and 4.0 lack pgipfloat, but accept floats as pgipint*) |
|
55 |
val pgipstring = "pgipstring"; |
|
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 = |
51992 | 64 |
if typ = Options.boolT then pgipbool |
65 |
else if typ = Options.intT then pgipint |
|
66 |
else if typ = Options.realT then pgipfloat |
|
67 |
else pgipstring; |
|
51944 | 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 |
||
51992 | 89 |
val bool_pref = generic_pref Markup.print_bool Markup.parse_bool pgipbool; |
90 |
val int_pref = generic_pref Markup.print_int Markup.parse_int pgipint; |
|
91 |
val real_pref = generic_pref Markup.print_real Markup.parse_real pgipfloat; |
|
92 |
val string_pref = generic_pref I I pgipstring; |
|
28587 | 93 |
|
94 |
||
95 |
(* preferences of Pure *) |
|
21637 | 96 |
|
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39165
diff
changeset
|
97 |
val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () => |
28587 | 98 |
let |
51991
5b814dd90f7f
prefer Markup.parse/print operations -- slight change of exception behaviour;
wenzelm
parents:
51971
diff
changeset
|
99 |
fun get () = Markup.print_bool (Proofterm.proofs_enabled ()); |
5b814dd90f7f
prefer Markup.parse/print operations -- slight change of exception behaviour;
wenzelm
parents:
51971
diff
changeset
|
100 |
fun set s = Proofterm.proofs := (if Markup.parse_bool s then 2 else 1); |
51992 | 101 |
in mkpref get set pgipbool "full-proofs" "Record full proof objects internally" end) (); |
21637 | 102 |
|
32061
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset
|
103 |
val parallel_proof_pref = |
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset
|
104 |
let |
51991
5b814dd90f7f
prefer Markup.parse/print operations -- slight change of exception behaviour;
wenzelm
parents:
51971
diff
changeset
|
105 |
fun get () = Markup.print_bool (! Goal.parallel_proofs >= 1); |
5b814dd90f7f
prefer Markup.parse/print operations -- slight change of exception behaviour;
wenzelm
parents:
51971
diff
changeset
|
106 |
fun set s = Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0); |
51992 | 107 |
in mkpref get set pgipbool "parallel-proofs" "Check proofs in parallel" end; |
32061
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset
|
108 |
|
28587 | 109 |
val thm_depsN = "thm_deps"; |
24329 | 110 |
val thm_deps_pref = |
28587 | 111 |
let |
51991
5b814dd90f7f
prefer Markup.parse/print operations -- slight change of exception behaviour;
wenzelm
parents:
51971
diff
changeset
|
112 |
fun get () = Markup.print_bool (print_mode_active thm_depsN); |
28587 | 113 |
fun set s = |
51991
5b814dd90f7f
prefer Markup.parse/print operations -- slight change of exception behaviour;
wenzelm
parents:
51971
diff
changeset
|
114 |
if Markup.parse_bool s |
32738 | 115 |
then Unsynchronized.change print_mode (insert (op =) thm_depsN) |
116 |
else Unsynchronized.change print_mode (remove (op =) thm_depsN); |
|
28587 | 117 |
in |
51992 | 118 |
mkpref get set pgipbool "theorem-dependencies" |
28587 | 119 |
"Track theorem dependencies within Proof General" |
120 |
end; |
|
21637 | 121 |
|
122 |
val print_depth_pref = |
|
28587 | 123 |
let |
51991
5b814dd90f7f
prefer Markup.parse/print operations -- slight change of exception behaviour;
wenzelm
parents:
51971
diff
changeset
|
124 |
val get = Markup.print_int o get_print_depth; |
5b814dd90f7f
prefer Markup.parse/print operations -- slight change of exception behaviour;
wenzelm
parents:
51971
diff
changeset
|
125 |
val set = print_depth o Markup.parse_int; |
51992 | 126 |
in mkpref get set pgipint "print-depth" "Setting for the ML print depth" end; |
21637 | 127 |
|
128 |
||
24329 | 129 |
val display_preferences = |
42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
130 |
[bool_pref Printer.show_types_default |
28587 | 131 |
"show-types" |
132 |
"Include types in display of Isabelle terms", |
|
42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
133 |
bool_pref Printer.show_sorts_default |
28587 | 134 |
"show-sorts" |
135 |
"Include sorts in display of Isabelle terms", |
|
42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
136 |
bool_pref Goal_Display.show_consts_default |
28587 | 137 |
"show-consts" |
138 |
"Show types of consts in Isabelle goal display", |
|
51949
f6858bb224c9
some system options as context-sensitive config options;
wenzelm
parents:
51946
diff
changeset
|
139 |
options_pref "names_long" |
28587 | 140 |
"long-names" |
141 |
"Show fully qualified names in Isabelle terms", |
|
42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset
|
142 |
bool_pref Printer.show_brackets_default |
28587 | 143 |
"show-brackets" |
144 |
"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
|
145 |
bool_pref Goal_Display.show_main_goal_default |
28587 | 146 |
"show-main-goal" |
147 |
"Show main goal in proof state display", |
|
42284 | 148 |
bool_pref Syntax_Trans.eta_contract_default |
28587 | 149 |
"eta-contract" |
150 |
"Print terms eta-contracted"]; |
|
21637 | 151 |
|
152 |
val advanced_display_preferences = |
|
51960
61ac1efe02c3
option "goals_limit", with more uniform description;
wenzelm
parents:
51949
diff
changeset
|
153 |
[options_pref "goals_limit" |
28587 | 154 |
"goals-limit" |
51960
61ac1efe02c3
option "goals_limit", with more uniform description;
wenzelm
parents:
51949
diff
changeset
|
155 |
"Setting for maximum number of subgoals to be printed", |
28587 | 156 |
print_depth_pref, |
51949
f6858bb224c9
some system options as context-sensitive config options;
wenzelm
parents:
51946
diff
changeset
|
157 |
options_pref "show_question_marks" |
28587 | 158 |
"show-question-marks" |
159 |
"Show leading question mark of variable name"]; |
|
21637 | 160 |
|
24329 | 161 |
val tracing_preferences = |
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41227
diff
changeset
|
162 |
[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
|
163 |
"trace-simplifier" |
26e820d27e0a
re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
boehmes
parents:
35979
diff
changeset
|
164 |
"Trace simplification rules.", |
51971
716bb7e2e272
simplified preferences, removed obsolete operations;
wenzelm
parents:
51970
diff
changeset
|
165 |
int_pref Raw_Simplifier.simp_trace_depth_limit_default |
28587 | 166 |
"trace-simplifier-depth" |
167 |
"Trace simplifier depth limit.", |
|
168 |
bool_pref Pattern.trace_unify_fail |
|
169 |
"trace-unification" |
|
170 |
"Output error diagnostics during unification", |
|
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41698
diff
changeset
|
171 |
bool_pref Toplevel.timing |
28587 | 172 |
"global-timing" |
173 |
"Whether to enable timing in Isabelle.", |
|
174 |
bool_pref Toplevel.debug |
|
175 |
"debugging" |
|
176 |
"Whether to enable debugging.", |
|
177 |
thm_deps_pref]; |
|
21637 | 178 |
|
24329 | 179 |
val proof_preferences = |
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39165
diff
changeset
|
180 |
[Unsynchronized.setmp quick_and_dirty true (fn () => |
30980 | 181 |
bool_pref quick_and_dirty |
182 |
"quick-and-dirty" |
|
183 |
"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
|
184 |
bool_pref Goal.skip_proofs |
28587 | 185 |
"skip-proofs" |
48634 | 186 |
"Skip over proofs", |
28587 | 187 |
proof_pref, |
51971
716bb7e2e272
simplified preferences, removed obsolete operations;
wenzelm
parents:
51970
diff
changeset
|
188 |
int_pref Multithreading.max_threads |
28587 | 189 |
"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
|
190 |
"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
|
191 |
parallel_proof_pref]; |
21637 | 192 |
|
28587 | 193 |
val pure_preferences = |
30980 | 194 |
[(category_display, display_preferences), |
195 |
(category_advanced_display, advanced_display_preferences), |
|
196 |
(category_tracing, tracing_preferences), |
|
197 |
(category_proof, proof_preferences)]; |
|
21637 | 198 |
|
28587 | 199 |
|
200 |
(* table of categories and preferences; names must be unique *) |
|
201 |
||
202 |
type T = (string * preference list) list; |
|
22214
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset
|
203 |
|
28587 | 204 |
fun add cname (pref: preference) (tab: T) = tab |> map |
205 |
(fn (cat, prefs) => |
|
206 |
if cat <> cname then (cat, prefs) |
|
207 |
else |
|
208 |
if exists (fn {name, ...} => name = #name pref) prefs |
|
28591 | 209 |
then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs)) |
30985 | 210 |
else (cat, prefs @ [pref])); |
28066
611e504c1191
extended interface to preferences to allow adding new ones
nipkow
parents:
25440
diff
changeset
|
211 |
|
28587 | 212 |
end; |