| author | wenzelm |
| Thu, 16 May 2013 21:48:01 +0200 | |
| changeset 52043 | 286629271d65 |
| parent 52017 | bc0238c1f73a |
| child 52059 | 2f970c7f722b |
| permissions | -rw-r--r-- |
| 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 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
5 |
Proof General preferences for Isabelle/Pure. |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
6 |
*) |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
7 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
8 |
(* display *) |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
9 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
10 |
val _ = |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
11 |
ProofGeneral.preference_option ProofGeneral.category_display |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
12 |
NONE |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
13 |
@{option show_types}
|
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
14 |
"show-types" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
15 |
"Include types in display of Isabelle terms"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
16 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
17 |
val _ = |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
18 |
ProofGeneral.preference_option ProofGeneral.category_display |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
19 |
NONE |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
20 |
@{option show_sorts}
|
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
21 |
"show-sorts" |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
22 |
"Include sorts in display of Isabelle types"; |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
23 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
24 |
val _ = |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
25 |
ProofGeneral.preference_option ProofGeneral.category_display |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
26 |
NONE |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
27 |
@{option show_consts}
|
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
28 |
"show-consts" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
29 |
"Show types of consts in Isabelle goal display"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
30 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
31 |
val _ = |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
32 |
ProofGeneral.preference_option ProofGeneral.category_display |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
33 |
NONE |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
34 |
@{option names_long}
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
35 |
"long-names" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
36 |
"Show fully qualified names in Isabelle terms"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
37 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
38 |
val _ = |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
39 |
ProofGeneral.preference_option ProofGeneral.category_display |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
40 |
NONE |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
41 |
@{option show_brackets}
|
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
42 |
"show-brackets" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
43 |
"Show full bracketing in Isabelle terms"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
44 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
45 |
val _ = |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
46 |
ProofGeneral.preference_option ProofGeneral.category_display |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
47 |
NONE |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
48 |
@{option show_main_goal}
|
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
49 |
"show-main-goal" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
50 |
"Show main goal in proof state display"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
51 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
52 |
val _ = |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
53 |
ProofGeneral.preference_option ProofGeneral.category_display |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
54 |
NONE |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
55 |
@{option eta_contract}
|
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
56 |
"eta-contract" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
57 |
"Print terms eta-contracted"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
58 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
59 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
60 |
(* advanced display *) |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
61 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
62 |
val _ = |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
63 |
ProofGeneral.preference_option ProofGeneral.category_advanced_display |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
64 |
NONE |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
65 |
@{option goals_limit}
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
66 |
"goals-limit" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
67 |
"Setting for maximum number of subgoals to be printed"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
68 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
69 |
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
|
70 |
ProofGeneral.preference ProofGeneral.category_advanced_display |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
71 |
NONE |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
72 |
(Markup.print_int o get_print_depth) |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
73 |
(print_depth o Markup.parse_int) |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
74 |
ProofGeneral.pgipint |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
75 |
"print-depth" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
76 |
"Setting for the ML print depth"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
77 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
78 |
val _ = |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
79 |
ProofGeneral.preference_option ProofGeneral.category_advanced_display |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
80 |
NONE |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
81 |
@{option show_question_marks}
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
82 |
"show-question-marks" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
83 |
"Show leading question mark of variable name"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
84 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
85 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
86 |
(* tracing *) |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
87 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
88 |
val _ = |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
89 |
ProofGeneral.preference_bool ProofGeneral.category_tracing |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
90 |
NONE |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
91 |
Raw_Simplifier.simp_trace_default |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
92 |
"trace-simplifier" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
93 |
"Trace simplification rules"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
94 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
95 |
val _ = |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
96 |
ProofGeneral.preference_int ProofGeneral.category_tracing |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
97 |
NONE |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
98 |
Raw_Simplifier.simp_trace_depth_limit_default |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
99 |
"trace-simplifier-depth" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
100 |
"Trace simplifier depth limit"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
101 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
102 |
val _ = |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
103 |
ProofGeneral.preference_bool ProofGeneral.category_tracing |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
104 |
NONE |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
105 |
Pattern.trace_unify_fail |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
106 |
"trace-unification" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
107 |
"Output error diagnostics during unification"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
108 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
109 |
val _ = |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
110 |
ProofGeneral.preference_bool ProofGeneral.category_tracing |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
111 |
NONE |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
112 |
Toplevel.timing |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
113 |
"global-timing" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
114 |
"Whether to enable timing in Isabelle"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
115 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
116 |
val _ = |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
117 |
ProofGeneral.preference_bool ProofGeneral.category_tracing |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
118 |
NONE |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
119 |
Toplevel.debug |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
120 |
"debugging" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
121 |
"Whether to enable debugging"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
122 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
123 |
val _ = |
| 52011 | 124 |
ProofGeneral.preference_bool ProofGeneral.category_tracing |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
125 |
NONE |
| 52011 | 126 |
ProofGeneral.thm_deps |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
127 |
"theorem-dependencies" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
128 |
"Track theorem dependencies within Proof General"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
129 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
130 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
131 |
(* proof *) |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
132 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
133 |
val _ = |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
134 |
ProofGeneral.preference_bool ProofGeneral.category_proof |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
135 |
(SOME "true") |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
136 |
quick_and_dirty |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
137 |
"quick-and-dirty" |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
138 |
"Take a few short cuts"; |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
139 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
140 |
val _ = |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
141 |
ProofGeneral.preference_bool ProofGeneral.category_proof |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
142 |
NONE |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
143 |
Goal.skip_proofs |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
144 |
"skip-proofs" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
145 |
"Skip over proofs"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
146 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
147 |
val _ = |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
148 |
ProofGeneral.preference ProofGeneral.category_proof |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
149 |
NONE |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
150 |
(Markup.print_bool o Proofterm.proofs_enabled) |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
151 |
(fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1)) |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
152 |
ProofGeneral.pgipbool |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
153 |
"full-proofs" |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
154 |
"Record full proof objects internally"; |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
155 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
156 |
val _ = |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
157 |
ProofGeneral.preference_int ProofGeneral.category_proof |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
158 |
NONE |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
159 |
Multithreading.max_threads |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
160 |
"max-threads" |
|
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
161 |
"Maximum number of threads"; |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
162 |
|
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
163 |
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
|
164 |
ProofGeneral.preference ProofGeneral.category_proof |
|
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52016
diff
changeset
|
165 |
NONE |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
166 |
(fn () => Markup.print_bool (! Goal.parallel_proofs >= 1)) |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
167 |
(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
|
168 |
ProofGeneral.pgipbool |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
169 |
"parallel-proofs" |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
170 |
"Check proofs in parallel"; |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
171 |