author | wenzelm |
Sat, 05 Jul 2014 16:29:19 +0200 | |
changeset 58865 | 1767b0f3b29b |
parent 58217 | f6259d6fb565 |
child 59083 | abae8aff6262 |
permissions | -rw-r--r-- |
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@53883 | 9 |
-- "build document in given format: pdf, dvi, 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 thy_output_display : bool = false |
wenzelm@49595 | 18 |
-- "indicate output as multi-line display-style material" |
wenzelm@49810 | 19 |
option thy_output_break : bool = false |
wenzelm@49595 | 20 |
-- "control line breaks in non-display material" |
wenzelm@49810 | 21 |
option thy_output_quotes : bool = false |
wenzelm@49595 | 22 |
-- "indicate if the output should be enclosed in double quotes" |
wenzelm@49810 | 23 |
option thy_output_indent : int = 0 |
wenzelm@49595 | 24 |
-- "indentation for pretty printing of display material" |
wenzelm@49810 | 25 |
option thy_output_source : bool = false |
wenzelm@49595 | 26 |
-- "print original source text rather than internal representation" |
wenzelm@53179 | 27 |
option thy_output_modes : string = "" |
wenzelm@53179 | 28 |
-- "additional print modes for document output (separated by commas)" |
wenzelm@50285 | 29 |
|
wenzelm@53180 | 30 |
|
wenzelm@53180 | 31 |
section "Prover Output" |
wenzelm@53180 | 32 |
|
wenzelm@53180 | 33 |
option show_types : bool = false |
wenzelm@53180 | 34 |
-- "show type constraints when printing terms" |
wenzelm@53180 | 35 |
option show_sorts : bool = false |
wenzelm@53180 | 36 |
-- "show sort constraints when printing types" |
wenzelm@53180 | 37 |
option show_brackets : bool = false |
wenzelm@53180 | 38 |
-- "show extra brackets when printing terms/types" |
wenzelm@53180 | 39 |
option show_question_marks : bool = true |
wenzelm@53180 | 40 |
-- "show leading question mark of schematic variables" |
wenzelm@53180 | 41 |
|
wenzelm@53180 | 42 |
option show_consts : bool = false |
wenzelm@53180 | 43 |
-- "show constants with types when printing proof state" |
wenzelm@53180 | 44 |
option show_main_goal : bool = false |
wenzelm@53180 | 45 |
-- "show main goal when printing proof state" |
wenzelm@53180 | 46 |
option goals_limit : int = 10 |
wenzelm@53180 | 47 |
-- "maximum number of subgoals to be printed" |
wenzelm@53180 | 48 |
|
wenzelm@53180 | 49 |
option names_long : bool = false |
wenzelm@53180 | 50 |
-- "show fully qualified names" |
wenzelm@53180 | 51 |
option names_short : bool = false |
wenzelm@53180 | 52 |
-- "show base names only" |
wenzelm@53180 | 53 |
option names_unique : bool = true |
wenzelm@53180 | 54 |
-- "show partially qualified names, as required for unique name resolution" |
wenzelm@53180 | 55 |
|
wenzelm@53180 | 56 |
option eta_contract : bool = true |
wenzelm@53180 | 57 |
-- "print terms in eta-contracted form" |
wenzelm@53180 | 58 |
|
wenzelm@53180 | 59 |
option pretty_margin : int = 76 |
wenzelm@53180 | 60 |
-- "right margin / page width of pretty printer in Isabelle/ML" |
wenzelm@53180 | 61 |
|
wenzelm@50285 | 62 |
option print_mode : string = "" |
wenzelm@50285 | 63 |
-- "additional print modes for prover output (separated by commas)" |
wenzelm@50285 | 64 |
|
wenzelm@50285 | 65 |
|
wenzelm@58217 | 66 |
section "Parallel Processing" |
wenzelm@50285 | 67 |
|
wenzelm@53202 | 68 |
public option threads : int = 0 |
wenzelm@50285 | 69 |
-- "maximum number of worker threads for prover process (0 = hardware max.)" |
wenzelm@58076 | 70 |
option threads_trace : int = 0 |
wenzelm@50285 | 71 |
-- "level of tracing information for multithreading" |
wenzelm@58217 | 72 |
public option parallel_print : bool = true |
wenzelm@58217 | 73 |
-- "parallel and asynchronous printing of results" |
wenzelm@53202 | 74 |
public option parallel_proofs : int = 2 |
wenzelm@50285 | 75 |
-- "level of parallel proof checking: 0, 1, 2" |
wenzelm@53851 | 76 |
option parallel_subproofs_threshold : real = 0.01 |
wenzelm@52560 | 77 |
-- "lower bound of timing estimate for forked nested proofs (seconds)" |
wenzelm@50285 | 78 |
|
wenzelm@50285 | 79 |
|
wenzelm@53627 | 80 |
section "Detail of Proof Checking" |
wenzelm@50285 | 81 |
|
wenzelm@50285 | 82 |
option quick_and_dirty : bool = false |
wenzelm@50285 | 83 |
-- "if true then some tools will OMIT some proofs" |
wenzelm@50285 | 84 |
option skip_proofs : bool = false |
wenzelm@52690 | 85 |
-- "skip over proofs (implicit 'sorry')" |
wenzelm@50285 | 86 |
|
wenzelm@50285 | 87 |
|
wenzelm@50310 | 88 |
section "Global Session Parameters" |
wenzelm@50285 | 89 |
|
wenzelm@50285 | 90 |
option condition : string = "" |
wenzelm@50285 | 91 |
-- "required environment variables for subsequent theories (separated by commas)" |
wenzelm@50285 | 92 |
|
wenzelm@49810 | 93 |
option timing : bool = false |
wenzelm@49595 | 94 |
-- "global timing of toplevel command execution and theory processing" |
wenzelm@49507 | 95 |
|
wenzelm@49810 | 96 |
option timeout : real = 0 |
wenzelm@49676 | 97 |
-- "timeout for session build job (seconds > 0)" |
wenzelm@49676 | 98 |
|
wenzelm@53099 | 99 |
option process_output_limit : int = 100 |
wenzelm@53099 | 100 |
-- "build process output limit in million characters (0 = unlimited)" |
wenzelm@53099 | 101 |
|
wenzelm@57621 | 102 |
|
wenzelm@57621 | 103 |
section "ML System" |
wenzelm@57621 | 104 |
|
wenzelm@57621 | 105 |
public option ML_exception_trace : bool = false |
wenzelm@57621 | 106 |
-- "ML exception trace for toplevel command execution" |
wenzelm@57607 | 107 |
|
wenzelm@50303 | 108 |
|
wenzelm@50310 | 109 |
section "Editor Reactivity" |
wenzelm@50303 | 110 |
|
wenzelm@53202 | 111 |
public option editor_load_delay : real = 0.5 |
wenzelm@50303 | 112 |
-- "delay for file load operations (new buffers etc.)" |
wenzelm@50303 | 113 |
|
wenzelm@53202 | 114 |
public option editor_input_delay : real = 0.3 |
wenzelm@50303 | 115 |
-- "delay for user input (text edits, cursor movement etc.)" |
wenzelm@50303 | 116 |
|
wenzelm@53202 | 117 |
public option editor_output_delay : real = 0.1 |
wenzelm@50303 | 118 |
-- "delay for prover output (markup, common messages etc.)" |
wenzelm@50303 | 119 |
|
wenzelm@53202 | 120 |
public option editor_update_delay : real = 0.5 |
wenzelm@50303 | 121 |
-- "delay for physical GUI updates" |
wenzelm@50303 | 122 |
|
wenzelm@53202 | 123 |
public option editor_reparse_limit : int = 10000 |
wenzelm@50539 | 124 |
-- "maximum amount of reparsed text outside perspective" |
wenzelm@51134 | 125 |
|
wenzelm@53202 | 126 |
public option editor_tracing_messages : int = 1000 |
wenzelm@51520 | 127 |
-- "initial number of tracing messages for each command transaction" |
wenzelm@51712 | 128 |
|
wenzelm@53202 | 129 |
public option editor_chart_delay : real = 3.0 |
wenzelm@51712 | 130 |
-- "delay for chart repainting" |
wenzelm@53839 | 131 |
|
wenzelm@53944 | 132 |
public option editor_continuous_checking : bool = true |
wenzelm@53944 | 133 |
-- "continuous checking of proof document (visible and required parts)" |
wenzelm@53944 | 134 |
|
wenzelm@53935 | 135 |
option editor_execution_delay : real = 0.02 |
wenzelm@53935 | 136 |
-- "delay for start of execution process after document update (seconds)" |
wenzelm@53935 | 137 |
|
wenzelm@53839 | 138 |
|
wenzelm@53839 | 139 |
section "Miscellaneous Tools" |
wenzelm@53839 | 140 |
|
wenzelm@53839 | 141 |
public option find_theorems_limit : int = 40 |
wenzelm@53839 | 142 |
-- "limit of displayed results" |
wenzelm@53839 | 143 |
|
wenzelm@57955 | 144 |
public option find_theorems_tactic_limit : int = 5 |
wenzelm@53839 | 145 |
-- "limit of tactic search for 'solves' criterion" |
wenzelm@53839 | 146 |
|
wenzelm@57014 | 147 |
|
wenzelm@57014 | 148 |
section "Completion" |
wenzelm@57014 | 149 |
|
wenzelm@57014 | 150 |
public option completion_limit : int = 40 |
wenzelm@57014 | 151 |
-- "limit for completion within the formal context" |
wenzelm@57014 | 152 |