author  wenzelm 
Tue, 31 Jul 2007 21:19:22 +0200  
changeset 24100  a2f19514e156 
parent 22587  5454b06320fb 
child 24191  333f0a4bcc55 
permissions  rwrr 
21637  1 
(* Title: Pure/ProofGeneral/preferences.ML 
2 
ID: $Id$ 

3 
Author: David Aspinall and Markus Wenzel 

4 

5 
User preferences for Isabelle which are maintained by the interface. 

6 
*) 

7 

8 
signature PREFERENCES = 

9 
sig 

10 
type pgiptype = PgipTypes.pgiptype 

11 

12 
type isa_preference = { name: string, 

13 
descr: string, 

14 
default: string, 

15 
pgiptype: pgiptype, 

16 
get: unit > string, 

17 
set: string > unit } 

18 

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

19 
(* table of categorised and preferences; names must be unique *) 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

20 
type isa_preference_table = (string * isa_preference list) list 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

21 

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

22 
val preferences : isa_preference_table 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

23 

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

24 
val remove : string > isa_preference_table > isa_preference_table 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

25 
val set_default : string * string > isa_preference_table > isa_preference_table 
21637  26 
end 
27 

28 
structure Preferences : PREFERENCES = 

29 
struct 

30 

31 
val thm_depsN = "thm_deps"; (* also in proof_general_pgip.ML: move to pgip_isabelle? *) 

32 

33 
type pgiptype = PgipTypes.pgiptype 

34 

35 
type isa_preference = { name: string, 

36 
descr: string, 

37 
default: string, 

38 
pgiptype: pgiptype, 

39 
get: unit > string, 

40 
set: string > unit } 

41 

42 

43 
fun mkpref get set typ nm descr = 

44 
{ name=nm, descr=descr, pgiptype=typ, get=get, set=set, default=get() } : isa_preference 

45 

46 
fun mkpref_from_ref read write typ r nm descr = 

47 
mkpref (fn()=> read (!r)) (fn v=> r:= (write v)) typ nm descr 

48 

49 
val int_pref = 

50 
mkpref_from_ref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE,NONE)) 

51 
(PgipTypes.Pgipint (NONE, NONE)) 

52 
val nat_pref = 

53 
mkpref_from_ref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat 

54 

55 
val bool_pref = 

56 
mkpref_from_ref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool 

57 

58 
val proof_pref = 

59 
let 

60 
fun get () = PgipTypes.bool_to_pgstring (! proofs >= 2) 

21940  61 
fun set s = proofs := (if PgipTypes.read_pgipbool s then 1 else 2) 
21637  62 
in 
63 
mkpref get set PgipTypes.Pgipbool "fullproofs" 

64 
"Record full proof objects internally" 

65 
end 

66 

67 
val thm_deps_pref = 

68 
let 

22587  69 
fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN) 
21940  70 
fun set s = if PgipTypes.read_pgipbool s then 
21637  71 
change print_mode (insert (op =) thm_depsN) 
72 
else 

73 
change print_mode (remove (op =) thm_depsN) 

74 
in 

75 
mkpref get set PgipTypes.Pgipbool "theoremdependencies" 

76 
"Track theorem dependencies within Proof General" 

77 
end 

78 

79 
val print_depth_pref = 

80 
let 

81 
val pg_print_depth_val = ref 10 

82 
fun get () = PgipTypes.int_to_pgstring (! pg_print_depth_val) 

83 
fun setn n = (print_depth n; pg_print_depth_val := n) 

84 
val set = setn o PgipTypes.read_pgipnat 

85 
in 

21649
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset

86 
mkpref get set PgipTypes.Pgipnat 
40e6fdd26f82
Support PGIP communication for preferences in Emacs mode.
aspinall
parents:
21637
diff
changeset

87 
"printdepth" "Setting for the ML print depth" 
21637  88 
end 
89 

90 

91 
val display_preferences = 

92 
[bool_pref show_types 

93 
"showtypes" 

94 
"Include types in display of Isabelle terms", 

95 
bool_pref show_sorts 

96 
"showsorts" 

97 
"Include sorts in display of Isabelle terms", 

98 
bool_pref show_consts 

99 
"showconsts" 

100 
"Show types of consts in Isabelle goal display", 

101 
bool_pref long_names 

102 
"longnames" 

103 
"Show fully qualified names in Isabelle terms", 

104 
bool_pref show_brackets 

105 
"showbrackets" 

106 
"Show full bracketing in Isabelle terms", 

107 
bool_pref Proof.show_main_goal 

108 
"showmaingoal" 

109 
"Show main goal in proof state display", 

110 
bool_pref Syntax.eta_contract 

111 
"etacontract" 

112 
"Print terms etacontracted"] 

113 

114 
val advanced_display_preferences = 

115 
[nat_pref goals_limit 

116 
"goalslimit" 

117 
"Setting for maximum number of goals printed", 

118 
int_pref ProofContext.prems_limit 

119 
"premslimit" 

120 
"Setting for maximum number of premises printed", 

121 
print_depth_pref, 

122 
bool_pref show_question_marks 

123 
"showquestionmarks" 

124 
"Show leading question mark of variable name"] 

125 

126 
val tracing_preferences = 

127 
[bool_pref trace_simp 

128 
"tracesimplifier" 

129 
"Trace simplification rules.", 

130 
nat_pref trace_simp_depth_limit 

131 
"tracesimplifierdepth" 

132 
"Trace simplifier depth limit.", 

133 
bool_pref trace_rules 

134 
"tracerules" 

135 
"Trace application of the standard rules", 

136 
bool_pref Pattern.trace_unify_fail 

137 
"traceunification" 

138 
"Output error diagnostics during unification", 

139 
bool_pref Output.timing 

140 
"globaltiming" 

141 
"Whether to enable timing in Isabelle.", 

22130  142 
bool_pref Toplevel.debug 
143 
"debugging" 

144 
"Whether to enable debugging."] 

21637  145 

146 
val proof_preferences = 

147 
[bool_pref quick_and_dirty 

148 
"quickanddirty" 

149 
"Take a few short cuts", 

150 
bool_pref Toplevel.skip_proofs 

151 
"skipproofs" 

24100  152 
"Skip over proofs (interactiveonly)", 
153 
nat_pref Multithreading.max_threads 

154 
"maxthreads" 

155 
"Maximum number of threads"] 

21637  156 

157 
val preferences = 

158 
[("Display", display_preferences), 

159 
("Advanced Display", advanced_display_preferences), 

160 
("Tracing", tracing_preferences), 

161 
("Proof", proof_preferences)] 

162 

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

163 
type isa_preference_table = (string * isa_preference list) list 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

164 

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

165 
fun remove name (preftable : isa_preference_table) = 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

166 
map (fn (cat,prefs) => 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

167 
(cat, filter_out (curry op= name o #name) prefs)) 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

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

169 

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

170 
fun set_default (setname,newdefault) (preftable : isa_preference_table) = 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

171 
map (fn (cat,prefs) => 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

172 
(cat, map (fn (pref as {name,descr,default,pgiptype,get,set}) 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

173 
=> if (name = setname) then 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

174 
(set newdefault; 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

175 
{name=name,descr=descr,default=newdefault, 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

176 
pgiptype=pgiptype,get=get,set=set}) 
6e9ab159512f
Add operations on preference tables (remove, set_default).
aspinall
parents:
22130
diff
changeset

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

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

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

180 

21637  181 
end 