author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 48634  30a6e841390a 
child 51944  45b972dc7888 
permissions  rwrr 
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} 

20 
val generic_pref: ('a > string) > (string > 'a) > PgipTypes.pgiptype > 

32738  21 
'a Unsynchronized.ref > string > string > preference 
22 
val string_pref: string Unsynchronized.ref > string > string > preference 

40292  23 
val real_pref: real Unsynchronized.ref > string > string > preference 
32738  24 
val int_pref: int Unsynchronized.ref > string > string > preference 
25 
val nat_pref: int Unsynchronized.ref > string > string > preference 

26 
val bool_pref: bool Unsynchronized.ref > string > string > preference 

28587  27 
type T = (string * preference list) list 
28 
val pure_preferences: T 

29 
val remove: string > T > T 

30 
val add: string > preference > T > T 

31 
val set_default: string * string > T > T 

21637  32 
end 
33 

28587  34 
structure Preferences: PREFERENCES = 
21637  35 
struct 
36 

30980  37 
(* categories *) 
38 

39 
val category_display = "Display"; 

40 
val category_advanced_display = "Advanced Display"; 

41 
val category_tracing = "Tracing"; 

42 
val category_proof = "Proof" 

43 

44 

28587  45 
(* preferences and preference tables *) 
21637  46 

28587  47 
type preference = 
48 
{name: string, 

49 
descr: string, 

50 
default: string, 

51 
pgiptype: PgipTypes.pgiptype, 

52 
get: unit > string, 

53 
set: string > unit}; 

54 

55 
fun mkpref raw_get raw_set typ name descr : preference = 

56 
let 

57 
fun get () = CRITICAL raw_get; 

58 
fun set x = CRITICAL (fn () => raw_set x); 

59 
in {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()} end; 

21637  60 

61 

28587  62 
(* generic preferences *) 
21637  63 

28587  64 
fun generic_pref read write typ r = 
65 
mkpref (fn () => read (! r)) (fn x => r := write x) typ; 

66 

67 
val string_pref = generic_pref I I PgipTypes.Pgipstring; 

21637  68 

40292  69 
val real_pref = 
70 
generic_pref PgipTypes.real_to_pgstring PgipTypes.read_pgipreal PgipTypes.Pgipreal; 

71 

24329  72 
val int_pref = 
28587  73 
generic_pref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE, NONE)) 
74 
(PgipTypes.Pgipint (NONE, NONE)); 

75 

21637  76 
val nat_pref = 
28587  77 
generic_pref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat; 
21637  78 

79 
val bool_pref = 

28587  80 
generic_pref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool; 
81 

82 

83 
(* preferences of Pure *) 

21637  84 

39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39165
diff
changeset

85 
val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () => 
28587  86 
let 
41698  87 
fun get () = PgipTypes.bool_to_pgstring (Proofterm.proofs_enabled ()); 
28587  88 
fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1); 
30980  89 
in mkpref get set PgipTypes.Pgipbool "fullproofs" "Record full proof objects internally" end) (); 
21637  90 

32061
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset

91 
val parallel_proof_pref = 
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset

92 
let 
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset

93 
fun get () = PgipTypes.bool_to_pgstring (! Goal.parallel_proofs >= 1); 
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset

94 
fun set s = Goal.parallel_proofs := (if PgipTypes.read_pgipbool s then 1 else 0); 
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset

95 
in mkpref get set PgipTypes.Pgipbool "parallelproofs" "Check proofs in parallel" end; 
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset

96 

28587  97 
val thm_depsN = "thm_deps"; 
24329  98 
val thm_deps_pref = 
28587  99 
let 
100 
fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN); 

101 
fun set s = 

32738  102 
if PgipTypes.read_pgipbool s 
103 
then Unsynchronized.change print_mode (insert (op =) thm_depsN) 

104 
else Unsynchronized.change print_mode (remove (op =) thm_depsN); 

28587  105 
in 
106 
mkpref get set PgipTypes.Pgipbool "theoremdependencies" 

107 
"Track theorem dependencies within Proof General" 

108 
end; 

21637  109 

110 
val print_depth_pref = 

28587  111 
let 
112 
fun get () = PgipTypes.int_to_pgstring (get_print_depth ()); 

113 
val set = print_depth o PgipTypes.read_pgipnat; 

114 
in mkpref get set PgipTypes.Pgipnat "printdepth" "Setting for the ML print depth" end; 

21637  115 

116 

24329  117 
val display_preferences = 
42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset

118 
[bool_pref Printer.show_types_default 
28587  119 
"showtypes" 
120 
"Include types in display of Isabelle terms", 

42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset

121 
bool_pref Printer.show_sorts_default 
28587  122 
"showsorts" 
123 
"Include sorts in display of Isabelle terms", 

42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset

124 
bool_pref Goal_Display.show_consts_default 
28587  125 
"showconsts" 
126 
"Show types of consts in Isabelle goal display", 

42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42358
diff
changeset

127 
bool_pref Name_Space.names_long_default 
28587  128 
"longnames" 
129 
"Show fully qualified names in Isabelle terms", 

42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset

130 
bool_pref Printer.show_brackets_default 
28587  131 
"showbrackets" 
132 
"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

133 
bool_pref Goal_Display.show_main_goal_default 
28587  134 
"showmaingoal" 
135 
"Show main goal in proof state display", 

42284  136 
bool_pref Syntax_Trans.eta_contract_default 
28587  137 
"etacontract" 
138 
"Print terms etacontracted"]; 

21637  139 

140 
val advanced_display_preferences = 

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

141 
[nat_pref Goal_Display.goals_limit_default 
28587  142 
"goalslimit" 
143 
"Setting for maximum number of goals printed", 

144 
print_depth_pref, 

42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
42284
diff
changeset

145 
bool_pref Printer.show_question_marks_default 
28587  146 
"showquestionmarks" 
147 
"Show leading question mark of variable name"]; 

21637  148 

24329  149 
val tracing_preferences = 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41227
diff
changeset

150 
[bool_pref Raw_Simplifier.simp_trace_default 
35995
26e820d27e0a
reintroduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
boehmes
parents:
35979
diff
changeset

151 
"tracesimplifier" 
26e820d27e0a
reintroduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
boehmes
parents:
35979
diff
changeset

152 
"Trace simplification rules.", 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41227
diff
changeset

153 
nat_pref Raw_Simplifier.simp_trace_depth_limit_default 
28587  154 
"tracesimplifierdepth" 
155 
"Trace simplifier depth limit.", 

156 
bool_pref Pattern.trace_unify_fail 

157 
"traceunification" 

158 
"Output error diagnostics during unification", 

42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41698
diff
changeset

159 
bool_pref Toplevel.timing 
28587  160 
"globaltiming" 
161 
"Whether to enable timing in Isabelle.", 

162 
bool_pref Toplevel.debug 

163 
"debugging" 

164 
"Whether to enable debugging.", 

165 
thm_deps_pref]; 

21637  166 

24329  167 
val proof_preferences = 
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39165
diff
changeset

168 
[Unsynchronized.setmp quick_and_dirty true (fn () => 
30980  169 
bool_pref quick_and_dirty 
170 
"quickanddirty" 

171 
"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

172 
bool_pref Goal.skip_proofs 
28587  173 
"skipproofs" 
48634  174 
"Skip over proofs", 
28587  175 
proof_pref, 
176 
nat_pref Multithreading.max_threads 

177 
"maxthreads" 

29435
a5f84ac14609
added parallel_proofs flag (default true, cf. usedir option Q), which can be disabled in lowmemory situations;
wenzelm
parents:
28591
diff
changeset

178 
"Maximum number of threads", 
32061
11f8ee55662d
parallel_proofs: more finegrained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
30985
diff
changeset

179 
parallel_proof_pref]; 
21637  180 

28587  181 
val pure_preferences = 
30980  182 
[(category_display, display_preferences), 
183 
(category_advanced_display, advanced_display_preferences), 

184 
(category_tracing, tracing_preferences), 

185 
(category_proof, proof_preferences)]; 

21637  186 

28587  187 

188 
(* table of categories and preferences; names must be unique *) 

189 

190 
type T = (string * preference list) list; 

22214
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

191 

28587  192 
fun remove name (tab: T) = tab > map 
193 
(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

194 

28587  195 
fun set_default (setname, newdefault) (tab: T) = tab > map 
196 
(fn (cat, prefs) => 

197 
(cat, prefs > map (fn (pref as {name, descr, default, pgiptype, get, set}) => 

198 
if name = setname then 

199 
(set newdefault; 

200 
{name =name , descr = descr, default = newdefault, 

201 
pgiptype = pgiptype, get = get, set = set}) 

202 
else pref))); 

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; 