author | wenzelm |
Sat, 16 Oct 2021 20:21:13 +0200 | |
changeset 74532 | 64d1b02327a4 |
parent 74147 | d030b988d470 |
child 74732 | 015282fb3e31 |
permissions | -rw-r--r-- |
48367 | 1 |
(* :mode=isabelle-options: *) |
2 |
||
49295 | 3 |
section "Document Preparation" |
49270 | 4 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
5 |
option browser_info : bool = false |
48580 | 6 |
-- "generate theory browser information" |
48367 | 7 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
8 |
option document : string = "" |
73827 | 9 |
-- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")" |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48795
diff
changeset
|
10 |
option document_output : string = "" |
72578
3e8395f9093a
clarified build_doc, based on Present.build_documents;
wenzelm
parents:
72300
diff
changeset
|
11 |
-- "document output directory" |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48795
diff
changeset
|
12 |
option document_variants : string = "document" |
67137 | 13 |
-- "alternative document variants (separated by colons)" |
67138 | 14 |
option document_tags : string = "" |
15 |
-- "default command tags (separated by commas)" |
|
73743 | 16 |
option document_bibliography : bool = false |
17 |
-- "explicitly enable use of bibtex (default: according to presence of root.bib)" |
|
73735 | 18 |
option document_preprocessor : string = "" |
19 |
-- "document preprocessor: executable relative to document output directory" |
|
73721
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73701
diff
changeset
|
20 |
option document_build : string = "lualatex" |
52030acb19ac
option document_build refers to build engine in Isabelle/Scala;
wenzelm
parents:
73701
diff
changeset
|
21 |
-- "document build engine (e.g. lualatex, pdflatex, build)" |
73723 | 22 |
option document_logo : string = "" |
23 |
-- "generate named instance of Isabelle logo (underscore means unnamed variant)" |
|
48367 | 24 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
25 |
option thy_output_display : bool = false |
48580 | 26 |
-- "indicate output as multi-line display-style material" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
27 |
option thy_output_break : bool = false |
48580 | 28 |
-- "control line breaks in non-display material" |
70121 | 29 |
option thy_output_cartouche : bool = false |
30 |
-- "indicate if the output should be delimited as cartouche" |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
31 |
option thy_output_quotes : bool = false |
70121 | 32 |
-- "indicate if the output should be delimited via double quotes" |
59175
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
58849
diff
changeset
|
33 |
option thy_output_margin : int = 76 |
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
58849
diff
changeset
|
34 |
-- "right margin / page width for printing of display material" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
35 |
option thy_output_indent : int = 0 |
48580 | 36 |
-- "indentation for pretty printing of display material" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
37 |
option thy_output_source : bool = false |
48580 | 38 |
-- "print original source text rather than internal representation" |
70122
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset
|
39 |
option thy_output_source_cartouche : bool = false |
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset
|
40 |
-- "print original source text rather than internal representation, preserve cartouches" |
52042 | 41 |
option thy_output_modes : string = "" |
42 |
-- "additional print modes for document output (separated by commas)" |
|
49270 | 43 |
|
52043
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
44 |
|
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
45 |
section "Prover Output" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
46 |
|
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
47 |
option show_types : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
48 |
-- "show type constraints when printing terms" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
49 |
option show_sorts : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
50 |
-- "show sort constraints when printing types" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
51 |
option show_brackets : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
52 |
-- "show extra brackets when printing terms/types" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
53 |
option show_question_marks : bool = true |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
54 |
-- "show leading question mark of schematic variables" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
55 |
|
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
56 |
option show_consts : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
57 |
-- "show constants with types when printing proof state" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
58 |
option show_main_goal : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
59 |
-- "show main goal when printing proof state" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
60 |
option goals_limit : int = 10 |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
61 |
-- "maximum number of subgoals to be printed" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
62 |
|
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
63 |
option names_long : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
64 |
-- "show fully qualified names" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
65 |
option names_short : bool = false |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
66 |
-- "show base names only" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
67 |
option names_unique : bool = true |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
68 |
-- "show partially qualified names, as required for unique name resolution" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
69 |
|
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
70 |
option eta_contract : bool = true |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
71 |
-- "print terms in eta-contracted form" |
286629271d65
more system options as context-sensitive config options;
wenzelm
parents:
52042
diff
changeset
|
72 |
|
49270 | 73 |
option print_mode : string = "" |
74 |
-- "additional print modes for prover output (separated by commas)" |
|
75 |
||
76 |
||
73387 | 77 |
section "Parallel Processing and Timing" |
49270 | 78 |
|
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
79 |
public option threads : int = 0 |
49270 | 80 |
-- "maximum number of worker threads for prover process (0 = hardware max.)" |
56734
6ca87a061740
suppress potential dangerous option (see 1baa5d19ac44);
wenzelm
parents:
56613
diff
changeset
|
81 |
option threads_trace : int = 0 |
49270 | 82 |
-- "level of tracing information for multithreading" |
59468
fe6651760643
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents:
59446
diff
changeset
|
83 |
option threads_stack_limit : real = 0.25 |
fe6651760643
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents:
59446
diff
changeset
|
84 |
-- "maximum stack size for worker threads (in giga words, 0 = unlimited)" |
62790 | 85 |
|
68130
6fb85346cb79
clarified future scheduling parameters, with support for parallel_limit;
wenzelm
parents:
67743
diff
changeset
|
86 |
public option parallel_limit : int = 0 |
6fb85346cb79
clarified future scheduling parameters, with support for parallel_limit;
wenzelm
parents:
67743
diff
changeset
|
87 |
-- "approximative limit for parallel tasks (0 = unlimited)" |
56875
f6259d6fb565
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
wenzelm
parents:
56734
diff
changeset
|
88 |
public option parallel_print : bool = true |
f6259d6fb565
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
wenzelm
parents:
56734
diff
changeset
|
89 |
-- "parallel and asynchronous printing of results" |
65056 | 90 |
public option parallel_proofs : int = 1 |
49270 | 91 |
-- "level of parallel proof checking: 0, 1, 2" |
52714 | 92 |
option parallel_subproofs_threshold : real = 0.01 |
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51230
diff
changeset
|
93 |
-- "lower bound of timing estimate for forked nested proofs (seconds)" |
49270 | 94 |
|
66160 | 95 |
option command_timing_threshold : real = 0.1 |
62793
f235646b1b73
less bulky timing information, e.g. HOL 56913 ~> 672;
wenzelm
parents:
62790
diff
changeset
|
96 |
-- "default threshold for persistent command timing (seconds)" |
f235646b1b73
less bulky timing information, e.g. HOL 56913 ~> 672;
wenzelm
parents:
62790
diff
changeset
|
97 |
|
73387 | 98 |
public option timeout_scale : real = 1.0 |
99 |
-- "scale factor for timeout in Isabelle/ML and session build" |
|
100 |
||
49270 | 101 |
|
52490 | 102 |
section "Detail of Proof Checking" |
49270 | 103 |
|
65448
9bc3b57c1fa7
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents:
65264
diff
changeset
|
104 |
option record_proofs : int = -1 |
9bc3b57c1fa7
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents:
65264
diff
changeset
|
105 |
-- "set level of proofterm recording: 0, 1, 2, negative means unchanged" |
49270 | 106 |
option quick_and_dirty : bool = false |
107 |
-- "if true then some tools will OMIT some proofs" |
|
108 |
option skip_proofs : bool = false |
|
51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51423
diff
changeset
|
109 |
-- "skip over proofs (implicit 'sorry')" |
68661 | 110 |
option strict_facts : bool = false |
111 |
-- "force lazy facts when defined in context" |
|
49270 | 112 |
|
113 |
||
49295 | 114 |
section "Global Session Parameters" |
49270 | 115 |
|
116 |
option condition : string = "" |
|
117 |
-- "required environment variables for subsequent theories (separated by commas)" |
|
118 |
||
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
119 |
option timeout : real = 0 |
48661 | 120 |
-- "timeout for session build job (seconds > 0)" |
121 |
||
73701 | 122 |
option timeout_build : bool = true |
123 |
-- "observe timeout for session build" |
|
124 |
||
51962
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51960
diff
changeset
|
125 |
option process_output_limit : int = 100 |
62409
e391528eff3b
proper option process_output_tail, more generous default;
wenzelm
parents:
62115
diff
changeset
|
126 |
-- "build process output limit (in million characters, 0 = unlimited)" |
e391528eff3b
proper option process_output_tail, more generous default;
wenzelm
parents:
62115
diff
changeset
|
127 |
|
e391528eff3b
proper option process_output_tail, more generous default;
wenzelm
parents:
62115
diff
changeset
|
128 |
option process_output_tail : int = 40 |
e391528eff3b
proper option process_output_tail, more generous default;
wenzelm
parents:
62115
diff
changeset
|
129 |
-- "build process output tail shown to user (in lines, 0 = unlimited)" |
51962
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51960
diff
changeset
|
130 |
|
64308 | 131 |
option profiling : string = "" |
132 |
-- "ML profiling (possible values: time, allocations)" |
|
133 |
||
73777
52e43a93d51f
clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
wenzelm
parents:
73743
diff
changeset
|
134 |
option system_log : string = "" |
73827 | 135 |
-- "output for system messages (log file or \"true\" for console progress)" |
73777
52e43a93d51f
clarified system_log: make this work independently of the particular "isabelle build" command-line (e.g. "isabelle mirabelle");
wenzelm
parents:
73743
diff
changeset
|
136 |
|
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69755
diff
changeset
|
137 |
option system_heaps : bool = false |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69755
diff
changeset
|
138 |
-- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69755
diff
changeset
|
139 |
|
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
|
140 |
|
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
|
141 |
section "ML System" |
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
|
142 |
|
62711 | 143 |
option ML_print_depth : int = 20 |
144 |
-- "ML print depth for toplevel pretty-printing" |
|
145 |
||
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
|
146 |
public option ML_exception_trace : bool = false |
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
|
147 |
-- "ML exception trace for toplevel command execution" |
56265
785569927666
discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents:
55672
diff
changeset
|
148 |
|
62498 | 149 |
public option ML_exception_debugger : bool = false |
150 |
-- "ML debugger exception trace for toplevel command execution" |
|
151 |
||
60730 | 152 |
public option ML_debugger : bool = false |
153 |
-- "ML debugger instrumentation for newly compiled code" |
|
154 |
||
61158
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
60889
diff
changeset
|
155 |
public option ML_system_64 : bool = false |
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
60889
diff
changeset
|
156 |
-- "ML system for 64bit platform is used if possible (change requires restart)" |
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
60889
diff
changeset
|
157 |
|
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63827
diff
changeset
|
158 |
public option ML_process_policy : string = "" |
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63827
diff
changeset
|
159 |
-- "ML process command prefix (process policy)" |
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63827
diff
changeset
|
160 |
|
49288 | 161 |
|
71675 | 162 |
section "PIDE Build" |
163 |
||
164 |
option pide_reports : bool = true |
|
165 |
-- "report PIDE markup" |
|
166 |
||
72892
d15c0c7ae092
full PIDE reports in batch build: see how it impacts overall performance;
wenzelm
parents:
72728
diff
changeset
|
167 |
option build_pide_reports : bool = true |
72728
caa182bdab7a
clarified options: batch-build has pide_reports disabled by default (requires significant resources);
wenzelm
parents:
72675
diff
changeset
|
168 |
-- "report PIDE markup in batch build" |
caa182bdab7a
clarified options: batch-build has pide_reports disabled by default (requires significant resources);
wenzelm
parents:
72675
diff
changeset
|
169 |
|
71675 | 170 |
|
69520 | 171 |
section "Editor Session" |
49288 | 172 |
|
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
173 |
public option editor_load_delay : real = 0.5 |
49288 | 174 |
-- "delay for file load operations (new buffers etc.)" |
175 |
||
72933 | 176 |
public option editor_input_delay : real = 0.2 |
49288 | 177 |
-- "delay for user input (text edits, cursor movement etc.)" |
178 |
||
64524
e6a3c55b929b
explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents:
64325
diff
changeset
|
179 |
public option editor_generated_input_delay : real = 1.0 |
e6a3c55b929b
explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents:
64325
diff
changeset
|
180 |
-- "delay for machine-generated input that may outperform user edits" |
e6a3c55b929b
explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents:
64325
diff
changeset
|
181 |
|
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
182 |
public option editor_output_delay : real = 0.1 |
49288 | 183 |
-- "delay for prover output (markup, common messages etc.)" |
184 |
||
70787 | 185 |
public option editor_consolidate_delay : real = 2.0 |
66379
6392766f3c25
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents:
66160
diff
changeset
|
186 |
-- "delay to consolidate status of command evaluation (execution forks)" |
6392766f3c25
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents:
66160
diff
changeset
|
187 |
|
62115
57895801cb57
prune old versions more often, to reduce overall heap requirements;
wenzelm
parents:
61873
diff
changeset
|
188 |
public option editor_prune_delay : real = 15 |
57867
abae8aff6262
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
wenzelm
parents:
56875
diff
changeset
|
189 |
-- "delay to prune history (delete old versions)" |
abae8aff6262
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
wenzelm
parents:
56875
diff
changeset
|
190 |
|
65264
7e6ecd04b5fe
dynamic session_options for tuning parameters and initial prover options;
wenzelm
parents:
65141
diff
changeset
|
191 |
option editor_prune_size : int = 0 |
7e6ecd04b5fe
dynamic session_options for tuning parameters and initial prover options;
wenzelm
parents:
65141
diff
changeset
|
192 |
-- "retained size of pruned history (delete old versions)" |
7e6ecd04b5fe
dynamic session_options for tuning parameters and initial prover options;
wenzelm
parents:
65141
diff
changeset
|
193 |
|
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
194 |
public option editor_update_delay : real = 0.5 |
49288 | 195 |
-- "delay for physical GUI updates" |
196 |
||
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
197 |
public option editor_reparse_limit : int = 10000 |
49524
68796a77c42b
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
wenzelm
parents:
49295
diff
changeset
|
198 |
-- "maximum amount of reparsed text outside perspective" |
50119
5c370a036de7
more generous tracing_limit, with explicit system option;
wenzelm
parents:
49524
diff
changeset
|
199 |
|
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
200 |
public option editor_tracing_messages : int = 1000 |
69103
814a1ab42d70
unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;
wenzelm
parents:
68661
diff
changeset
|
201 |
-- "initial number of tracing messages for each command transaction (0: unbounded)" |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50505
diff
changeset
|
202 |
|
52065
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents:
52043
diff
changeset
|
203 |
public option editor_chart_delay : real = 3.0 |
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50505
diff
changeset
|
204 |
-- "delay for chart repainting" |
52702 | 205 |
|
52807
b859a180936b
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
wenzelm
parents:
52798
diff
changeset
|
206 |
public option editor_continuous_checking : bool = true |
b859a180936b
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
wenzelm
parents:
52798
diff
changeset
|
207 |
-- "continuous checking of proof document (visible and required parts)" |
b859a180936b
simplified flag for continuous checking: avoid GUI complexity and slow checking of all theories (including prints);
wenzelm
parents:
52798
diff
changeset
|
208 |
|
61604 | 209 |
public option editor_output_state : bool = false |
61213 | 210 |
-- "implicit output of proof state" |
211 |
||
52798
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52779
diff
changeset
|
212 |
option editor_execution_delay : real = 0.02 |
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52779
diff
changeset
|
213 |
-- "delay for start of execution process after document update (seconds)" |
9d3c9862d1dd
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
wenzelm
parents:
52779
diff
changeset
|
214 |
|
57974 | 215 |
option editor_syslog_limit : int = 100 |
216 |
-- "maximum amount of buffered syslog messages" |
|
217 |
||
68197 | 218 |
public option editor_presentation : bool = false |
219 |
-- "dynamic presentation while editing" |
|
68184
6c693b2700b3
support for dynamic document output while editing;
wenzelm
parents:
68154
diff
changeset
|
220 |
|
52702 | 221 |
|
69520 | 222 |
section "Headless Session" |
223 |
||
70787 | 224 |
option headless_consolidate_delay : real = 15 |
225 |
-- "delay to consolidate status of command evaluation (execution forks)" |
|
226 |
||
227 |
option headless_prune_delay : real = 60 |
|
228 |
-- "delay to prune history (delete old versions)" |
|
229 |
||
69520 | 230 |
option headless_check_delay : real = 0.5 |
231 |
-- "delay for theory status check during PIDE processing (seconds)" |
|
232 |
||
233 |
option headless_check_limit : int = 0 |
|
234 |
-- "maximum number of theory status checks (0 = unlimited)" |
|
235 |
||
236 |
option headless_nodes_status_delay : real = -1 |
|
237 |
-- "delay for overall nodes status check during PIDE processing (seconds, disabled for < 0)" |
|
238 |
||
239 |
option headless_watchdog_timeout : real = 600 |
|
240 |
-- "watchdog timeout for PIDE processing of broken theories (seconds, 0 = disabled)" |
|
241 |
||
242 |
option headless_commit_cleanup_delay : real = 60 |
|
243 |
-- "delay for cleanup of already imported theories (seconds, 0 = disabled)" |
|
244 |
||
70801 | 245 |
option headless_load_limit : real = 5.0 |
70800 | 246 |
-- "limit in MB for loaded theory files (0 = unlimited)" |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70634
diff
changeset
|
247 |
|
69520 | 248 |
|
52702 | 249 |
section "Miscellaneous Tools" |
250 |
||
251 |
public option find_theorems_limit : int = 40 |
|
252 |
-- "limit of displayed results" |
|
253 |
||
56613 | 254 |
public option find_theorems_tactic_limit : int = 5 |
52702 | 255 |
-- "limit of tactic search for 'solves' criterion" |
256 |
||
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
53189
diff
changeset
|
257 |
|
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
53189
diff
changeset
|
258 |
section "Completion" |
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
53189
diff
changeset
|
259 |
|
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
53189
diff
changeset
|
260 |
public option completion_limit : int = 40 |
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
53189
diff
changeset
|
261 |
-- "limit for completion within the formal context" |
64130 | 262 |
|
66158 | 263 |
public option completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" |
264 |
-- "glob patterns to ignore in file-system path completion (separated by colons)" |
|
265 |
||
64130 | 266 |
|
65141 | 267 |
section "Spell Checker" |
268 |
||
269 |
public option spell_checker : bool = true |
|
270 |
-- "enable spell-checker for prose words within document text, comments etc." |
|
271 |
||
272 |
public option spell_checker_dictionary : string = "en" |
|
273 |
-- "spell-checker dictionary name" |
|
274 |
||
69353 | 275 |
public option spell_checker_include : string = "words,comment,comment1,comment2,comment3,ML_comment,SML_comment" |
67395
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67273
diff
changeset
|
276 |
-- "included markup elements for spell-checker (separated by commas)" |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67273
diff
changeset
|
277 |
|
70229 | 278 |
public option spell_checker_exclude : string = "document_marker,antiquoted,raw_text" |
67395
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67273
diff
changeset
|
279 |
-- "excluded markup elements for spell-checker (separated by commas)" |
65141 | 280 |
|
281 |
||
64130 | 282 |
section "Secure Shell" |
283 |
||
69431 | 284 |
option ssh_config_dir : string = "$HOME/.ssh" |
64130 | 285 |
-- "SSH configuration directory" |
286 |
||
69431 | 287 |
option ssh_config_file : string = "$HOME/.ssh/config" |
64130 | 288 |
-- "main SSH configuration file" |
289 |
||
69431 | 290 |
option ssh_identity_files : string = "$HOME/.ssh/id_dsa:$HOME/.ssh/id_ecdsa:$HOME/.ssh/id_rsa" |
64130 | 291 |
-- "possible SSH identity files (separated by colons)" |
292 |
||
293 |
option ssh_compression : bool = true |
|
294 |
-- "enable SSH compression" |
|
295 |
||
296 |
option ssh_connect_timeout : real = 60 |
|
297 |
-- "SSH connection timeout (seconds)" |
|
64325 | 298 |
|
299 |
option ssh_alive_interval : real = 30 |
|
300 |
-- "time interval to keep SSH server connection alive (seconds)" |
|
65595 | 301 |
|
67273
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents:
67194
diff
changeset
|
302 |
option ssh_alive_count_max : int = 3 |
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents:
67194
diff
changeset
|
303 |
-- "maximum number of messages to keep SSH server connection alive" |
c573cfb2c407
more robust connection: prefer ServerAliveCountMax=3 (ssh default) instead of 1 (jsch default);
wenzelm
parents:
67194
diff
changeset
|
304 |
|
65595 | 305 |
|
71422
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
306 |
section "Phabricator" |
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
307 |
|
74138 | 308 |
option phabricator_version_arcanist : string = "4f70fcffa8a5393e210d64f237ffdaa256256d6a" |
71422
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
309 |
-- "repository version for arcanist" |
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
310 |
|
74138 | 311 |
option phabricator_version_phabricator : string = "193798385bd3a7f72dca255e44f8112f4f8fc155" |
71422
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
312 |
-- "repository version for phabricator" |
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
313 |
|
5d5be87330b5
allow to override repository versions at runtime;
wenzelm
parents:
71068
diff
changeset
|
314 |
|
68221 | 315 |
section "Theory Export" |
68154 | 316 |
|
317 |
option export_theory : bool = false |
|
70396 | 318 |
-- "export theory content to Isabelle/Scala" |
319 |
||
70914
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70801
diff
changeset
|
320 |
option export_standard_proofs : bool = false |
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70801
diff
changeset
|
321 |
-- "export standardized proof terms to Isabelle/Scala (not scalable)" |
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70801
diff
changeset
|
322 |
|
70396 | 323 |
option export_proofs : bool = false |
324 |
-- "export proof terms to Isabelle/Scala" |
|
325 |
||
326 |
option prune_proofs : bool = false |
|
327 |
-- "prune proof terms after export (do not store in Isabelle/ML)" |
|
68154 | 328 |
|
329 |
||
69586
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69572
diff
changeset
|
330 |
section "Theory update" |
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69572
diff
changeset
|
331 |
|
69589
e15f053a42d8
support for isabelle update -u inner_syntax_cartouches;
wenzelm
parents:
69586
diff
changeset
|
332 |
option update_inner_syntax_cartouches : bool = false |
e15f053a42d8
support for isabelle update -u inner_syntax_cartouches;
wenzelm
parents:
69586
diff
changeset
|
333 |
-- "update inner syntax (types, terms, etc.) to use cartouches" |
e15f053a42d8
support for isabelle update -u inner_syntax_cartouches;
wenzelm
parents:
69586
diff
changeset
|
334 |
|
69586
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69572
diff
changeset
|
335 |
option update_mixfix_cartouches : bool = false |
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69572
diff
changeset
|
336 |
-- "update mixfix templates to use cartouches instead of double quotes" |
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69572
diff
changeset
|
337 |
|
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69589
diff
changeset
|
338 |
option update_control_cartouches : bool = false |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69589
diff
changeset
|
339 |
-- "update antiquotations to use control symbol with cartouche argument" |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69589
diff
changeset
|
340 |
|
69603 | 341 |
option update_path_cartouches : bool = false |
342 |
-- "update file-system paths to use cartouches" |
|
343 |
||
69586
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69572
diff
changeset
|
344 |
|
68221 | 345 |
section "Build Database" |
346 |
||
347 |
option build_database_server : bool = false |
|
348 |
option build_database_user : string = "" |
|
349 |
option build_database_password : string = "" |
|
350 |
option build_database_name : string = "" |
|
351 |
option build_database_host : string = "" |
|
352 |
option build_database_port : int = 0 |
|
353 |
option build_database_ssh_host : string = "" |
|
354 |
option build_database_ssh_user : string = "" |
|
355 |
option build_database_ssh_port : int = 0 |
|
356 |
||
357 |
||
65595 | 358 |
section "Build Log Database" |
359 |
||
360 |
option build_log_database_user : string = "" |
|
361 |
option build_log_database_password : string = "" |
|
362 |
option build_log_database_name : string = "" |
|
363 |
option build_log_database_host : string = "" |
|
364 |
option build_log_database_port : int = 0 |
|
365 |
option build_log_ssh_host : string = "" |
|
366 |
option build_log_ssh_user : string = "" |
|
367 |
option build_log_ssh_port : int = 0 |
|
65782 | 368 |
option build_log_history : int = 30 -- "length of relevant history (in days)" |
67743 | 369 |
option build_log_transaction_size : int = 1 -- "number of log files for each db update" |
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69520
diff
changeset
|
370 |
|
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69520
diff
changeset
|
371 |
|
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69520
diff
changeset
|
372 |
section "Isabelle/Scala/ML system channel" |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69520
diff
changeset
|
373 |
|
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69520
diff
changeset
|
374 |
option system_channel_address : string = "" |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69520
diff
changeset
|
375 |
option system_channel_password : string = "" |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74138
diff
changeset
|
376 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74138
diff
changeset
|
377 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74138
diff
changeset
|
378 |
section "Bash process execution server" |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74138
diff
changeset
|
379 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74138
diff
changeset
|
380 |
option bash_process_debugging : bool = false |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74138
diff
changeset
|
381 |
option bash_process_address : string = "" |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74138
diff
changeset
|
382 |
option bash_process_password : string = "" |