author | wenzelm |
Tue, 25 Mar 2014 19:03:02 +0100 | |
changeset 56281 | 03c3d1a7c3b8 |
parent 56279 | b4d874f6c6be |
child 56285 | 9315d3988d73 |
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 |
|
53403
c09f4005d6bd
some explicit indication of Proof General legacy;
wenzelm
parents:
52710
diff
changeset
|
8 |
(*Proof General legacy*) |
c09f4005d6bd
some explicit indication of Proof General legacy;
wenzelm
parents:
52710
diff
changeset
|
9 |
|
52437
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
10 |
structure ProofGeneral_Pure: sig end = |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
11 |
struct |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
12 |
|
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
13 |
(** preferences **) |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
14 |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
15 |
(* display *) |
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_types} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
21 |
"show-types" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
22 |
"Include types in display of Isabelle terms"; |
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_sorts} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
28 |
"show-sorts" |
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
29 |
"Include sorts in display of Isabelle types"; |
52007
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 _ = |
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
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 |
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
34 |
@{option show_consts} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
35 |
"show-consts" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
36 |
"Show types of consts in Isabelle goal display"; |
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 _ = |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
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 |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
41 |
@{option names_long} |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
42 |
"long-names" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
43 |
"Show fully qualified names 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_brackets} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
49 |
"show-brackets" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
50 |
"Show full bracketing in Isabelle terms"; |
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 show_main_goal} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
56 |
"show-main-goal" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
57 |
"Show main goal in proof state display"; |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
58 |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
59 |
val _ = |
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
60 |
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
|
61 |
NONE |
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52017
diff
changeset
|
62 |
@{option eta_contract} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
63 |
"eta-contract" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
64 |
"Print terms eta-contracted"; |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
65 |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
66 |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
67 |
(* advanced display *) |
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 _ = |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
70 |
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
|
71 |
NONE |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
72 |
@{option goals_limit} |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
73 |
"goals-limit" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
74 |
"Setting for maximum number of subgoals to be printed"; |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
75 |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
76 |
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
|
77 |
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
|
78 |
NONE |
56281 | 79 |
(Markup.print_int o get_default_print_depth) |
80 |
(put_default_print_depth o Markup.parse_int) |
|
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
81 |
ProofGeneral.pgipint |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
82 |
"print-depth" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
83 |
"Setting for the ML print depth"; |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
84 |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
85 |
val _ = |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
86 |
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
|
87 |
NONE |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
88 |
@{option show_question_marks} |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
89 |
"show-question-marks" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
90 |
"Show leading question mark of variable name"; |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
91 |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
92 |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
93 |
(* tracing *) |
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_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
|
97 |
NONE |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
98 |
Raw_Simplifier.simp_trace_default |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
99 |
"trace-simplifier" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
100 |
"Trace simplification rules"; |
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_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
|
104 |
NONE |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
105 |
Raw_Simplifier.simp_trace_depth_limit_default |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
106 |
"trace-simplifier-depth" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
107 |
"Trace simplifier depth limit"; |
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 |
52709
0e4bacf21e77
turned pattern unify flag into configuration option (global only);
wenzelm
parents:
52489
diff
changeset
|
112 |
Pattern.unify_trace_failure_default |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
113 |
"trace-unification" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
114 |
"Output error diagnostics during unification"; |
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.timing |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
120 |
"global-timing" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
121 |
"Whether to enable timing in Isabelle"; |
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 _ = |
56265
785569927666
discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents:
54717
diff
changeset
|
124 |
ProofGeneral.preference_option 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 |
56279
b4d874f6c6be
clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
wenzelm
parents:
56265
diff
changeset
|
126 |
@{option ML_exception_trace} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
127 |
"debugging" |
56265
785569927666
discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents:
54717
diff
changeset
|
128 |
"Whether to enable exception trace for toplevel command execution"; |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
129 |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
130 |
val _ = |
52011 | 131 |
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
|
132 |
NONE |
52011 | 133 |
ProofGeneral.thm_deps |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
134 |
"theorem-dependencies" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
135 |
"Track theorem dependencies within Proof General"; |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
136 |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
137 |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
138 |
(* proof *) |
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 _ = |
52059 | 141 |
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
|
142 |
(SOME "true") |
52059 | 143 |
@{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
|
144 |
"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
|
145 |
"Take a few short cuts"; |
52007
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 _ = |
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 |
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
|
149 |
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
|
150 |
@{option skip_proofs} |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
151 |
"skip-proofs" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
152 |
"Skip over proofs"; |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
153 |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
154 |
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
|
155 |
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
|
156 |
NONE |
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset
|
157 |
(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
|
158 |
(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
|
159 |
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
|
160 |
"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
|
161 |
"Record full proof objects internally"; |
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 _ = |
54717 | 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 |
54717 | 166 |
(Markup.print_int o Multithreading.max_threads_value) |
167 |
(Multithreading.max_threads_update o Markup.parse_int) |
|
168 |
ProofGeneral.pgipint |
|
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
|
169 |
"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
|
170 |
"Maximum number of threads"; |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
171 |
|
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
172 |
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
|
173 |
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
|
174 |
NONE |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
175 |
(fn () => Markup.print_bool (! Goal.parallel_proofs >= 1)) |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
176 |
(fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0)) |
54717 | 177 |
ProofGeneral.pgipint |
52007
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
178 |
"parallel-proofs" |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
179 |
"Check proofs in parallel"; |
0b1183012a3c
maintain ProofGeneral preferences within ProofGeneral module;
wenzelm
parents:
diff
changeset
|
180 |
|
52437
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
181 |
|
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
182 |
|
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
183 |
(** command syntax **) |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
184 |
|
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
185 |
val _ = |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
186 |
Outer_Syntax.improper_command |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
187 |
@{command_spec "ProofGeneral.process_pgip"} "(internal)" |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
188 |
(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
|
189 |
|
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
190 |
val _ = |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
191 |
Outer_Syntax.improper_command |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
192 |
@{command_spec "ProofGeneral.pr"} "(internal)" |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
193 |
(Scan.succeed (Toplevel.keep (fn state => |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
194 |
if Toplevel.is_toplevel state orelse Toplevel.is_theory state |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
195 |
then ProofGeneral.tell_clear_goals () |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
196 |
else (Toplevel.quiet := false; Toplevel.print_state true state)))); |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
197 |
|
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
198 |
val _ = (*undo without output -- historical*) |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
199 |
Outer_Syntax.improper_command |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
200 |
@{command_spec "ProofGeneral.undo"} "(internal)" |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
201 |
(Scan.succeed (Toplevel.imperative (fn () => Isar.undo 1))); |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
202 |
|
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
203 |
val _ = |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
204 |
Outer_Syntax.improper_command |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
205 |
@{command_spec "ProofGeneral.restart"} "(internal)" |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
206 |
(Parse.opt_unit >> (K (Toplevel.imperative ProofGeneral.restart))); |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
207 |
|
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
208 |
val _ = |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
209 |
Outer_Syntax.improper_command |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
210 |
@{command_spec "ProofGeneral.kill_proof"} "(internal)" |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
211 |
(Scan.succeed (Toplevel.imperative (fn () => |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
212 |
(Isar.kill_proof (); ProofGeneral.tell_clear_goals ())))); |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
213 |
|
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
214 |
val _ = |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
215 |
Outer_Syntax.improper_command |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
216 |
@{command_spec "ProofGeneral.inform_file_processed"} "(internal)" |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
217 |
(Parse.name >> (fn file => Toplevel.imperative (fn () => |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
218 |
ProofGeneral.inform_file_processed file))); |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
219 |
|
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
220 |
val _ = |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
221 |
Outer_Syntax.improper_command |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
222 |
@{command_spec "ProofGeneral.inform_file_retracted"} "(internal)" |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
223 |
(Parse.name >> (fn file => Toplevel.imperative (fn () => |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
224 |
ProofGeneral.inform_file_retracted file))); |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
225 |
|
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
226 |
end; |
c88354589b43
more formal ProofGeneral command setup within theory Pure;
wenzelm
parents:
52059
diff
changeset
|
227 |