wenzelm@49382
|
1 |
(* :mode=isabelle-options: *)
|
wenzelm@49382
|
2 |
|
wenzelm@50310
|
3 |
section "Document Preparation"
|
wenzelm@50285
|
4 |
|
wenzelm@49810
|
5 |
option browser_info : bool = false
|
wenzelm@49595
|
6 |
-- "generate theory browser information"
|
wenzelm@49382
|
7 |
|
wenzelm@49810
|
8 |
option document : string = ""
|
wenzelm@49595
|
9 |
-- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
|
wenzelm@49820
|
10 |
option document_output : string = ""
|
wenzelm@49820
|
11 |
-- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
|
wenzelm@49820
|
12 |
option document_variants : string = "document"
|
wenzelm@49810
|
13 |
-- "option alternative document variants (separated by colons)"
|
wenzelm@49810
|
14 |
option document_graph : bool = false
|
wenzelm@49595
|
15 |
-- "generate session graph image for document"
|
wenzelm@49382
|
16 |
|
wenzelm@49810
|
17 |
option show_question_marks : bool = true
|
wenzelm@49595
|
18 |
-- "show leading question mark of schematic variables"
|
wenzelm@49501
|
19 |
|
wenzelm@49810
|
20 |
option names_long : bool = false
|
wenzelm@49595
|
21 |
-- "show fully qualified names"
|
wenzelm@49810
|
22 |
option names_short : bool = false
|
wenzelm@49595
|
23 |
-- "show base names only"
|
wenzelm@49810
|
24 |
option names_unique : bool = true
|
wenzelm@49595
|
25 |
-- "show partially qualified names, as required for unique name resolution"
|
wenzelm@49501
|
26 |
|
wenzelm@49810
|
27 |
option pretty_margin : int = 76
|
wenzelm@49595
|
28 |
-- "right margin / page width of pretty printer in Isabelle/ML"
|
wenzelm@49542
|
29 |
|
wenzelm@49810
|
30 |
option thy_output_display : bool = false
|
wenzelm@49595
|
31 |
-- "indicate output as multi-line display-style material"
|
wenzelm@49810
|
32 |
option thy_output_break : bool = false
|
wenzelm@49595
|
33 |
-- "control line breaks in non-display material"
|
wenzelm@49810
|
34 |
option thy_output_quotes : bool = false
|
wenzelm@49595
|
35 |
-- "indicate if the output should be enclosed in double quotes"
|
wenzelm@49810
|
36 |
option thy_output_indent : int = 0
|
wenzelm@49595
|
37 |
-- "indentation for pretty printing of display material"
|
wenzelm@49810
|
38 |
option thy_output_source : bool = false
|
wenzelm@49595
|
39 |
-- "print original source text rather than internal representation"
|
wenzelm@49535
|
40 |
|
wenzelm@50285
|
41 |
|
wenzelm@50285
|
42 |
option print_mode : string = ""
|
wenzelm@50285
|
43 |
-- "additional print modes for prover output (separated by commas)"
|
wenzelm@50285
|
44 |
|
wenzelm@50285
|
45 |
|
wenzelm@50310
|
46 |
section "Parallel Checking"
|
wenzelm@50285
|
47 |
|
wenzelm@50285
|
48 |
option threads : int = 0
|
wenzelm@50285
|
49 |
-- "maximum number of worker threads for prover process (0 = hardware max.)"
|
wenzelm@50285
|
50 |
option threads_trace : int = 0
|
wenzelm@50285
|
51 |
-- "level of tracing information for multithreading"
|
wenzelm@50285
|
52 |
option parallel_proofs : int = 2
|
wenzelm@50285
|
53 |
-- "level of parallel proof checking: 0, 1, 2"
|
wenzelm@50285
|
54 |
option parallel_proofs_threshold : int = 100
|
wenzelm@50285
|
55 |
-- "threshold for sub-proof parallelization"
|
wenzelm@50285
|
56 |
|
wenzelm@50285
|
57 |
|
wenzelm@50310
|
58 |
section "Detail of Proof Recording"
|
wenzelm@50285
|
59 |
|
wenzelm@50285
|
60 |
option proofs : int = 1
|
wenzelm@50285
|
61 |
-- "level of detail for proof objects: 0, 1, 2"
|
wenzelm@50285
|
62 |
option quick_and_dirty : bool = false
|
wenzelm@50285
|
63 |
-- "if true then some tools will OMIT some proofs"
|
wenzelm@50285
|
64 |
option skip_proofs : bool = false
|
wenzelm@50285
|
65 |
-- "skip over proofs"
|
wenzelm@50285
|
66 |
|
wenzelm@50285
|
67 |
|
wenzelm@50310
|
68 |
section "Global Session Parameters"
|
wenzelm@50285
|
69 |
|
wenzelm@50285
|
70 |
option condition : string = ""
|
wenzelm@50285
|
71 |
-- "required environment variables for subsequent theories (separated by commas)"
|
wenzelm@50285
|
72 |
|
wenzelm@49810
|
73 |
option timing : bool = false
|
wenzelm@49595
|
74 |
-- "global timing of toplevel command execution and theory processing"
|
wenzelm@49507
|
75 |
|
wenzelm@49810
|
76 |
option timeout : real = 0
|
wenzelm@49676
|
77 |
-- "timeout for session build job (seconds > 0)"
|
wenzelm@49676
|
78 |
|
wenzelm@50303
|
79 |
|
wenzelm@50310
|
80 |
section "Editor Reactivity"
|
wenzelm@50303
|
81 |
|
wenzelm@50303
|
82 |
option editor_load_delay : real = 0.5
|
wenzelm@50303
|
83 |
-- "delay for file load operations (new buffers etc.)"
|
wenzelm@50303
|
84 |
|
wenzelm@50303
|
85 |
option editor_input_delay : real = 0.3
|
wenzelm@50303
|
86 |
-- "delay for user input (text edits, cursor movement etc.)"
|
wenzelm@50303
|
87 |
|
wenzelm@50303
|
88 |
option editor_output_delay : real = 0.1
|
wenzelm@50303
|
89 |
-- "delay for prover output (markup, common messages etc.)"
|
wenzelm@50303
|
90 |
|
wenzelm@50303
|
91 |
option editor_update_delay : real = 0.5
|
wenzelm@50303
|
92 |
-- "delay for physical GUI updates"
|
wenzelm@50303
|
93 |
|
wenzelm@50539
|
94 |
option editor_reparse_limit : int = 10000
|
wenzelm@50539
|
95 |
-- "maximum amount of reparsed text outside perspective"
|
wenzelm@51134
|
96 |
|
wenzelm@52012
|
97 |
option editor_tracing_messages : int = 1000
|
wenzelm@51520
|
98 |
-- "initial number of tracing messages for each command transaction"
|
wenzelm@51712
|
99 |
|
wenzelm@51712
|
100 |
option editor_chart_delay : real = 3.0
|
wenzelm@51712
|
101 |
-- "delay for chart repainting"
|