author | wenzelm |
Fri, 19 Jul 2013 17:35:12 +0200 | |
changeset 52709 | 0e4bacf21e77 |
parent 52489 | a36ba4d2819a |
child 52710 | 52790e3961fe |
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 |
|
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 context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
16 |
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
|
17 |
NONE |
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
18 |
@{option show_types} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
19 |
"show-types" |
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 context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
23 |
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
|
24 |
NONE |
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
25 |
@{option show_sorts} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
26 |
"show-sorts" |
52043
286629271d65
more system options as context-sensitive 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 context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
30 |
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
|
31 |
NONE |
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
32 |
@{option show_consts} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
33 |
"show-consts" |
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" 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
|
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 |
"long-names" |
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 context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
44 |
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
|
45 |
NONE |
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
46 |
@{option show_brackets} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
47 |
"show-brackets" |
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 context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
51 |
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
|
52 |
NONE |
52043
286629271d65
more system options as context-sensitive 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 |
"show-main-goal" |
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 context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
58 |
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
|
59 |
NONE |
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
60 |
@{option eta_contract} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
61 |
"eta-contract" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
62 |
"Print terms eta-contracted"; |
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" 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
|
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 |
"goals-limit" |
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" 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
|
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 |
"print-depth" |
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" 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
|
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 |
"show-question-marks" |
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" 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
|
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 |
"trace-simplifier" |
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" 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
|
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 |
"trace-simplifier-depth" |
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" 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
|
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 |
"trace-unification" |
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" 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
|
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 |
"global-timing" |
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" 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
|
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" 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
|
130 |
NONE |
52011 | 131 |
ProofGeneral.thm_deps |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
132 |
"theorem-dependencies" |
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" 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
|
140 |
(SOME "true") |
52059 | 141 |
@{option quick_and_dirty} |
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 |
"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
|
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 _ = |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
146 |
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
|
147 |
NONE |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
148 |
Goal.skip_proofs |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
149 |
"skip-proofs" |
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" 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 |
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
|
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" 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.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
|
158 |
"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
|
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" 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
|
162 |
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
|
163 |
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
|
164 |
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
|
165 |
"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
|
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" 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
|
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 |
"parallel-proofs" |
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 |