author  wenzelm 
Fri, 19 Jul 2013 17:58:57 +0200  
changeset 52710  52790e3961fe 
parent 52709  0e4bacf21e77 
child 53403  c09f4005d6bd 
permissions  rwrr 
52009  1 
(* Title: Pure/Tools/proof_general_pure.ML 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

2 
Author: David Aspinall 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

3 
Author: Makarius 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

4 

52437
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

5 
Proof General setup within theory Pure. 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

6 
*) 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

7 

52437
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

8 
structure ProofGeneral_Pure: sig end = 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

9 
struct 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

10 

c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

11 
(** preferences **) 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

12 

52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

13 
(* display *) 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

14 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

15 
val _ = 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

16 
ProofGeneral.preference_option ProofGeneral.category_display 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

17 
NONE 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

18 
@{option show_types} 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

19 
"showtypes" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

20 
"Include types in display of Isabelle terms"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

21 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

22 
val _ = 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

23 
ProofGeneral.preference_option ProofGeneral.category_display 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

24 
NONE 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

25 
@{option show_sorts} 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

26 
"showsorts" 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

27 
"Include sorts in display of Isabelle types"; 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

28 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

29 
val _ = 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

30 
ProofGeneral.preference_option ProofGeneral.category_display 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

31 
NONE 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

32 
@{option show_consts} 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

33 
"showconsts" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

34 
"Show types of consts in Isabelle goal display"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

35 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

36 
val _ = 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

37 
ProofGeneral.preference_option ProofGeneral.category_display 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

38 
NONE 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

39 
@{option names_long} 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

40 
"longnames" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

41 
"Show fully qualified names in Isabelle terms"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

42 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

43 
val _ = 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

44 
ProofGeneral.preference_option ProofGeneral.category_display 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

45 
NONE 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

46 
@{option show_brackets} 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

47 
"showbrackets" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

48 
"Show full bracketing in Isabelle terms"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

49 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

50 
val _ = 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

51 
ProofGeneral.preference_option ProofGeneral.category_display 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

52 
NONE 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

53 
@{option show_main_goal} 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

54 
"showmaingoal" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

55 
"Show main goal in proof state display"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

56 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

57 
val _ = 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

58 
ProofGeneral.preference_option ProofGeneral.category_display 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

59 
NONE 
52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52017
diff
changeset

60 
@{option eta_contract} 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

61 
"etacontract" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

62 
"Print terms etacontracted"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

63 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

64 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

65 
(* advanced display *) 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

66 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

67 
val _ = 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

68 
ProofGeneral.preference_option ProofGeneral.category_advanced_display 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

69 
NONE 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

70 
@{option goals_limit} 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

71 
"goalslimit" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

72 
"Setting for maximum number of subgoals to be printed"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

73 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

74 
val _ = 
52016
4b77f444afbb
simplified ProofGeneral.preference operation  no need for CRITICAL section for atomic access (and sequential execution of PG/TTY loop);
wenzelm
parents:
52011
diff
changeset

75 
ProofGeneral.preference ProofGeneral.category_advanced_display 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

76 
NONE 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

77 
(Markup.print_int o get_print_depth) 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

78 
(print_depth o Markup.parse_int) 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

79 
ProofGeneral.pgipint 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

80 
"printdepth" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

81 
"Setting for the ML print depth"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

82 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

83 
val _ = 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

84 
ProofGeneral.preference_option ProofGeneral.category_advanced_display 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

85 
NONE 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

86 
@{option show_question_marks} 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

87 
"showquestionmarks" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

88 
"Show leading question mark of variable name"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

89 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

90 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

91 
(* tracing *) 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

92 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

93 
val _ = 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

94 
ProofGeneral.preference_bool ProofGeneral.category_tracing 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

95 
NONE 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

96 
Raw_Simplifier.simp_trace_default 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

97 
"tracesimplifier" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

98 
"Trace simplification rules"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

99 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

100 
val _ = 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

101 
ProofGeneral.preference_int ProofGeneral.category_tracing 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

102 
NONE 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

103 
Raw_Simplifier.simp_trace_depth_limit_default 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

104 
"tracesimplifierdepth" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

105 
"Trace simplifier depth limit"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

106 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

107 
val _ = 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

108 
ProofGeneral.preference_bool ProofGeneral.category_tracing 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

109 
NONE 
52709
0e4bacf21e77
turned pattern unify flag into configuration option (global only);
wenzelm
parents:
52489
diff
changeset

110 
Pattern.unify_trace_failure_default 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

111 
"traceunification" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

112 
"Output error diagnostics during unification"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

113 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

114 
val _ = 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

115 
ProofGeneral.preference_bool ProofGeneral.category_tracing 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

116 
NONE 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

117 
Toplevel.timing 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

118 
"globaltiming" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

119 
"Whether to enable timing in Isabelle"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

120 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

121 
val _ = 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

122 
ProofGeneral.preference_bool ProofGeneral.category_tracing 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

123 
NONE 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

124 
Toplevel.debug 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

125 
"debugging" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

126 
"Whether to enable debugging"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

127 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

128 
val _ = 
52011  129 
ProofGeneral.preference_bool ProofGeneral.category_tracing 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

130 
NONE 
52011  131 
ProofGeneral.thm_deps 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

132 
"theoremdependencies" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

133 
"Track theorem dependencies within Proof General"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

134 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

135 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

136 
(* proof *) 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

137 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

138 
val _ = 
52059  139 
ProofGeneral.preference_option ProofGeneral.category_proof 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

140 
(SOME "true") 
52059  141 
@{option quick_and_dirty} 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

142 
"quickanddirty" 
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

143 
"Take a few short cuts"; 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

144 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

145 
val _ = 
52710
52790e3961fe
just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons  monotonic updates already handle goal forks smoothly);
wenzelm
parents:
52709
diff
changeset

146 
ProofGeneral.preference_option ProofGeneral.category_proof 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

147 
NONE 
52710
52790e3961fe
just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons  monotonic updates already handle goal forks smoothly);
wenzelm
parents:
52709
diff
changeset

148 
@{option skip_proofs} 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

149 
"skipproofs" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

150 
"Skip over proofs"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

151 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

152 
val _ = 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

153 
ProofGeneral.preference ProofGeneral.category_proof 
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

154 
NONE 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

155 
(Markup.print_bool o Proofterm.proofs_enabled) 
52489
a36ba4d2819a
more uniform notion of disabled proofs  NB: historic meaning of 1 for recording theorems is already included in 0;
wenzelm
parents:
52487
diff
changeset

156 
(fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 0)) 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

157 
ProofGeneral.pgipbool 
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

158 
"fullproofs" 
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

159 
"Record full proof objects internally"; 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

160 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

161 
val _ = 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

162 
ProofGeneral.preference_int ProofGeneral.category_proof 
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

163 
NONE 
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

164 
Multithreading.max_threads 
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

165 
"maxthreads" 
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

166 
"Maximum number of threads"; 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

167 

0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

168 
val _ = 
52016
4b77f444afbb
simplified ProofGeneral.preference operation  no need for CRITICAL section for atomic access (and sequential execution of PG/TTY loop);
wenzelm
parents:
52011
diff
changeset

169 
ProofGeneral.preference ProofGeneral.category_proof 
52017
bc0238c1f73a
clarified preferences: "override" reinitialized on prover startup, and "default" sent to PG  thus recover typical defaults like autoquickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset

170 
NONE 
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

171 
(fn () => Markup.print_bool (! Goal.parallel_proofs >= 1)) 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

172 
(fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0)) 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

173 
ProofGeneral.pgipbool 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

174 
"parallelproofs" 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

175 
"Check proofs in parallel"; 
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset

176 

52437
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

177 

c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

178 

c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

179 
(** command syntax **) 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

180 

c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

181 
val _ = 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

182 
Outer_Syntax.improper_command 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

183 
@{command_spec "ProofGeneral.process_pgip"} "(internal)" 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

184 
(Parse.text >> (fn str => Toplevel.imperative (fn () => ProofGeneral.process_pgip str))); 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

185 

c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

186 
val _ = 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

187 
Outer_Syntax.improper_command 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

188 
@{command_spec "ProofGeneral.pr"} "(internal)" 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

189 
(Scan.succeed (Toplevel.keep (fn state => 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

190 
if Toplevel.is_toplevel state orelse Toplevel.is_theory state 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

191 
then ProofGeneral.tell_clear_goals () 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

192 
else (Toplevel.quiet := false; Toplevel.print_state true state)))); 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

193 

c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

194 
val _ = (*undo without output  historical*) 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

195 
Outer_Syntax.improper_command 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

196 
@{command_spec "ProofGeneral.undo"} "(internal)" 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

197 
(Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1))); 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

198 

c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

199 
val _ = 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

200 
Outer_Syntax.improper_command 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

201 
@{command_spec "ProofGeneral.restart"} "(internal)" 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

202 
(Parse.opt_unit >> (K (Toplevel.imperative ProofGeneral.restart))); 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

203 

c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

204 
val _ = 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

205 
Outer_Syntax.improper_command 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

206 
@{command_spec "ProofGeneral.kill_proof"} "(internal)" 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

207 
(Scan.succeed (Toplevel.imperative (fn () => 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

208 
(Isar.kill_proof (); ProofGeneral.tell_clear_goals ())))); 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

209 

c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

210 
val _ = 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

211 
Outer_Syntax.improper_command 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

212 
@{command_spec "ProofGeneral.inform_file_processed"} "(internal)" 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

213 
(Parse.name >> (fn file => Toplevel.imperative (fn () => 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

214 
ProofGeneral.inform_file_processed file))); 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

215 

c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

216 
val _ = 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

217 
Outer_Syntax.improper_command 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

218 
@{command_spec "ProofGeneral.inform_file_retracted"} "(internal)" 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

219 
(Parse.name >> (fn file => Toplevel.imperative (fn () => 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

220 
ProofGeneral.inform_file_retracted file))); 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

221 

c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

222 
end; 
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset

223 