author | wenzelm |
Tue, 14 Aug 2012 15:42:58 +0200 | |
changeset 48805 | c3ea910b3581 |
parent 48795 | bece259ee055 |
child 49270 | e5d162d15867 |
permissions | -rw-r--r-- |
48367 | 1 |
(* :mode=isabelle-options: *) |
2 |
||
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
3 |
option browser_info : bool = false |
48580 | 4 |
-- "generate theory browser information" |
48367 | 5 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
6 |
option document : string = "" |
48580 | 7 |
-- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false" |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48795
diff
changeset
|
8 |
option document_output : string = "" |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48795
diff
changeset
|
9 |
-- "document output directory (default within $ISABELLE_BROWSER_INFO tree)" |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48795
diff
changeset
|
10 |
option document_variants : string = "document" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
11 |
-- "option alternative document variants (separated by colons)" |
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
12 |
option document_graph : bool = false |
48580 | 13 |
-- "generate session graph image for document" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
14 |
option document_dump : string = "" |
48580 | 15 |
-- "dump generated document sources into given directory" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
16 |
option document_dump_mode : string = "all" |
48580 | 17 |
-- "specific document dump mode: all, tex, tex+sty" |
48367 | 18 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
19 |
option threads : int = 0 |
48580 | 20 |
-- "maximum number of worker threads for prover process (0 = hardware max.)" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
21 |
option threads_trace : int = 0 |
48580 | 22 |
-- "level of tracing information for multithreading" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
23 |
option parallel_proofs : int = 2 |
48580 | 24 |
-- "level of parallel proof checking: 0, 1, 2" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
25 |
option parallel_proofs_threshold : int = 100 |
48580 | 26 |
-- "threshold for sub-proof parallelization" |
48367 | 27 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
28 |
option print_mode : string = "" |
48580 | 29 |
-- "additional print modes for prover output (separated by commas)" |
48367 | 30 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
31 |
option proofs : int = 1 |
48580 | 32 |
-- "level of detail for proof objects: 0, 1, 2" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
33 |
option quick_and_dirty : bool = false |
48580 | 34 |
-- "if true then some tools will OMIT some proofs" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
35 |
option skip_proofs : bool = false |
48634 | 36 |
-- "skip over proofs" |
48367 | 37 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
38 |
option condition : string = "" |
48580 | 39 |
-- "required environment variables for subsequent theories (separated by commas)" |
48367 | 40 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
41 |
option show_question_marks : bool = true |
48580 | 42 |
-- "show leading question mark of schematic variables" |
48486 | 43 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
44 |
option names_long : bool = false |
48580 | 45 |
-- "show fully qualified names" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
46 |
option names_short : bool = false |
48580 | 47 |
-- "show base names only" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
48 |
option names_unique : bool = true |
48580 | 49 |
-- "show partially qualified names, as required for unique name resolution" |
48486 | 50 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
51 |
option pretty_margin : int = 76 |
48580 | 52 |
-- "right margin / page width of pretty printer in Isabelle/ML" |
48527 | 53 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
54 |
option thy_output_display : bool = false |
48580 | 55 |
-- "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
|
56 |
option thy_output_break : bool = false |
48580 | 57 |
-- "control line breaks in non-display material" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
58 |
option thy_output_quotes : bool = false |
48580 | 59 |
-- "indicate if the output should be enclosed in double quotes" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
60 |
option thy_output_indent : int = 0 |
48580 | 61 |
-- "indentation for pretty printing of display material" |
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
62 |
option thy_output_source : bool = false |
48580 | 63 |
-- "print original source text rather than internal representation" |
48520 | 64 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
65 |
option timing : bool = false |
48580 | 66 |
-- "global timing of toplevel command execution and theory processing" |
48492 | 67 |
|
48795
bece259ee055
clarified format of etc/options: only declarations, not re-definitions;
wenzelm
parents:
48661
diff
changeset
|
68 |
option timeout : real = 0 |
48661 | 69 |
-- "timeout for session build job (seconds > 0)" |
70 |