1 (* :mode=isabelle-options: *) |
1 (* :mode=isabelle-options: *) |
|
2 |
|
3 section {* Document preparation *} |
2 |
4 |
3 option browser_info : bool = false |
5 option browser_info : bool = false |
4 -- "generate theory browser information" |
6 -- "generate theory browser information" |
5 |
7 |
6 option document : string = "" |
8 option document : string = "" |
13 -- "generate session graph image for document" |
15 -- "generate session graph image for document" |
14 option document_dump : string = "" |
16 option document_dump : string = "" |
15 -- "dump generated document sources into given directory" |
17 -- "dump generated document sources into given directory" |
16 option document_dump_mode : string = "all" |
18 option document_dump_mode : string = "all" |
17 -- "specific document dump mode: all, tex, tex+sty" |
19 -- "specific document dump mode: all, tex, tex+sty" |
18 |
|
19 option threads : int = 0 |
|
20 -- "maximum number of worker threads for prover process (0 = hardware max.)" |
|
21 option threads_trace : int = 0 |
|
22 -- "level of tracing information for multithreading" |
|
23 option parallel_proofs : int = 2 |
|
24 -- "level of parallel proof checking: 0, 1, 2" |
|
25 option parallel_proofs_threshold : int = 100 |
|
26 -- "threshold for sub-proof parallelization" |
|
27 |
|
28 option print_mode : string = "" |
|
29 -- "additional print modes for prover output (separated by commas)" |
|
30 |
|
31 option proofs : int = 1 |
|
32 -- "level of detail for proof objects: 0, 1, 2" |
|
33 option quick_and_dirty : bool = false |
|
34 -- "if true then some tools will OMIT some proofs" |
|
35 option skip_proofs : bool = false |
|
36 -- "skip over proofs" |
|
37 |
|
38 option condition : string = "" |
|
39 -- "required environment variables for subsequent theories (separated by commas)" |
|
40 |
20 |
41 option show_question_marks : bool = true |
21 option show_question_marks : bool = true |
42 -- "show leading question mark of schematic variables" |
22 -- "show leading question mark of schematic variables" |
43 |
23 |
44 option names_long : bool = false |
24 option names_long : bool = false |
60 option thy_output_indent : int = 0 |
40 option thy_output_indent : int = 0 |
61 -- "indentation for pretty printing of display material" |
41 -- "indentation for pretty printing of display material" |
62 option thy_output_source : bool = false |
42 option thy_output_source : bool = false |
63 -- "print original source text rather than internal representation" |
43 -- "print original source text rather than internal representation" |
64 |
44 |
|
45 |
|
46 option print_mode : string = "" |
|
47 -- "additional print modes for prover output (separated by commas)" |
|
48 |
|
49 |
|
50 section {* Parallel checking *} |
|
51 |
|
52 option threads : int = 0 |
|
53 -- "maximum number of worker threads for prover process (0 = hardware max.)" |
|
54 option threads_trace : int = 0 |
|
55 -- "level of tracing information for multithreading" |
|
56 option parallel_proofs : int = 2 |
|
57 -- "level of parallel proof checking: 0, 1, 2" |
|
58 option parallel_proofs_threshold : int = 100 |
|
59 -- "threshold for sub-proof parallelization" |
|
60 |
|
61 |
|
62 section {* Detail of proof recording *} |
|
63 |
|
64 option proofs : int = 1 |
|
65 -- "level of detail for proof objects: 0, 1, 2" |
|
66 option quick_and_dirty : bool = false |
|
67 -- "if true then some tools will OMIT some proofs" |
|
68 option skip_proofs : bool = false |
|
69 -- "skip over proofs" |
|
70 |
|
71 |
|
72 section {* Global session parameters *} |
|
73 |
|
74 option condition : string = "" |
|
75 -- "required environment variables for subsequent theories (separated by commas)" |
|
76 |
65 option timing : bool = false |
77 option timing : bool = false |
66 -- "global timing of toplevel command execution and theory processing" |
78 -- "global timing of toplevel command execution and theory processing" |
67 |
79 |
68 option timeout : real = 0 |
80 option timeout : real = 0 |
69 -- "timeout for session build job (seconds > 0)" |
81 -- "timeout for session build job (seconds > 0)" |