author  wenzelm 
Fri, 29 Dec 2006 18:25:46 +0100  
changeset 21940  fbd068dd4d29 
parent 21649  40e6fdd26f82 
child 22130  0906fd95e0b5 
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 

19 
val preferences : (string * isa_preference list) list 

20 
end 

21 

22 
structure Preferences : PREFERENCES = 

23 
struct 

24 

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

26 

27 
type pgiptype = PgipTypes.pgiptype 

28 

29 
type isa_preference = { name: string, 

30 
descr: string, 

31 
default: string, 

32 
pgiptype: pgiptype, 

33 
get: unit > string, 

34 
set: string > unit } 

35 

36 

37 
fun mkpref get set typ nm descr = 

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

39 

40 
fun mkpref_from_ref read write typ r nm descr = 

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

42 

43 
val int_pref = 

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

45 
(PgipTypes.Pgipint (NONE, NONE)) 

46 
val nat_pref = 

47 
mkpref_from_ref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat 

48 

49 
val bool_pref = 

50 
mkpref_from_ref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool 

51 

52 
val proof_pref = 

53 
let 

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

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

58 
"Record full proof objects internally" 

59 
end 

60 

61 
val thm_deps_pref = 

62 
let 

63 
fun get () = PgipTypes.bool_to_pgstring (Output.has_mode thm_depsN) 

21940  64 
fun set s = if PgipTypes.read_pgipbool s then 
21637  65 
change print_mode (insert (op =) thm_depsN) 
66 
else 

67 
change print_mode (remove (op =) thm_depsN) 

68 
in 

69 
mkpref get set PgipTypes.Pgipbool "theoremdependencies" 

70 
"Track theorem dependencies within Proof General" 

71 
end 

72 

73 
val print_depth_pref = 

74 
let 

75 
val pg_print_depth_val = ref 10 

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

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

78 
val set = setn o PgipTypes.read_pgipnat 

79 
in 

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

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

81 
"printdepth" "Setting for the ML print depth" 
21637  82 
end 
83 

84 

85 
val display_preferences = 

86 
[bool_pref show_types 

87 
"showtypes" 

88 
"Include types in display of Isabelle terms", 

89 
bool_pref show_sorts 

90 
"showsorts" 

91 
"Include sorts in display of Isabelle terms", 

92 
bool_pref show_consts 

93 
"showconsts" 

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

95 
bool_pref long_names 

96 
"longnames" 

97 
"Show fully qualified names in Isabelle terms", 

98 
bool_pref show_brackets 

99 
"showbrackets" 

100 
"Show full bracketing in Isabelle terms", 

101 
bool_pref Proof.show_main_goal 

102 
"showmaingoal" 

103 
"Show main goal in proof state display", 

104 
bool_pref Syntax.eta_contract 

105 
"etacontract" 

106 
"Print terms etacontracted"] 

107 

108 
val advanced_display_preferences = 

109 
[nat_pref goals_limit 

110 
"goalslimit" 

111 
"Setting for maximum number of goals printed", 

112 
int_pref ProofContext.prems_limit 

113 
"premslimit" 

114 
"Setting for maximum number of premises printed", 

115 
print_depth_pref, 

116 
bool_pref show_question_marks 

117 
"showquestionmarks" 

118 
"Show leading question mark of variable name"] 

119 

120 
val tracing_preferences = 

121 
[bool_pref trace_simp 

122 
"tracesimplifier" 

123 
"Trace simplification rules.", 

124 
nat_pref trace_simp_depth_limit 

125 
"tracesimplifierdepth" 

126 
"Trace simplifier depth limit.", 

127 
bool_pref trace_rules 

128 
"tracerules" 

129 
"Trace application of the standard rules", 

130 
bool_pref Pattern.trace_unify_fail 

131 
"traceunification" 

132 
"Output error diagnostics during unification", 

133 
bool_pref Output.timing 

134 
"globaltiming" 

135 
"Whether to enable timing in Isabelle.", 

136 
bool_pref Output.show_debug_msgs 

137 
"debugmessages" 

138 
"Whether to show debugging messages."] 

139 

140 
val proof_preferences = 

141 
[bool_pref quick_and_dirty 

142 
"quickanddirty" 

143 
"Take a few short cuts", 

144 
bool_pref Toplevel.skip_proofs 

145 
"skipproofs" 

21940  146 
"Skip over proofs (interactiveonly)"] 
21637  147 

148 
val preferences = 

149 
[("Display", display_preferences), 

150 
("Advanced Display", advanced_display_preferences), 

151 
("Tracing", tracing_preferences), 

152 
("Proof", proof_preferences)] 

153 

154 
end 