author  wenzelm 
Wed, 27 Mar 2013 16:46:52 +0100  
changeset 51554  041bc3d31f23 
parent 51553  63327f679cff 
child 51564  bfdc3f720bd6 
permissions  rwrr 
48367  1 
(* :mode=isabelleoptions: *) 
2 

49295  3 
section "Document Preparation" 
49270  4 

48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
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 redefinitions;
wenzelm
parents:
48661
diff
changeset

8 
option document : string = "" 
48580  9 
 "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

10 
option document_output : string = "" 
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48795
diff
changeset

11 
 "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

12 
option document_variants : string = "document" 
48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

13 
 "option alternative document variants (separated by colons)" 
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

14 
option document_graph : bool = false 
48580  15 
 "generate session graph image for document" 
48367  16 

48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

17 
option show_question_marks : bool = true 
48580  18 
 "show leading question mark of schematic variables" 
48486  19 

48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

20 
option names_long : bool = false 
48580  21 
 "show fully qualified names" 
48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

22 
option names_short : bool = false 
48580  23 
 "show base names only" 
48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

24 
option names_unique : bool = true 
48580  25 
 "show partially qualified names, as required for unique name resolution" 
48486  26 

48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

27 
option pretty_margin : int = 76 
48580  28 
 "right margin / page width of pretty printer in Isabelle/ML" 
48527  29 

48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

30 
option thy_output_display : bool = false 
48580  31 
 "indicate output as multiline displaystyle material" 
48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

32 
option thy_output_break : bool = false 
48580  33 
 "control line breaks in nondisplay material" 
48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

34 
option thy_output_quotes : bool = false 
48580  35 
 "indicate if the output should be enclosed in double quotes" 
48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

36 
option thy_output_indent : int = 0 
48580  37 
 "indentation for pretty printing of display material" 
48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

38 
option thy_output_source : bool = false 
48580  39 
 "print original source text rather than internal representation" 
48520  40 

49270  41 

42 
option print_mode : string = "" 

43 
 "additional print modes for prover output (separated by commas)" 

44 

45 

49295  46 
section "Parallel Checking" 
49270  47 

48 
option threads : int = 0 

49 
 "maximum number of worker threads for prover process (0 = hardware max.)" 

50 
option threads_trace : int = 0 

51 
 "level of tracing information for multithreading" 

52 
option parallel_proofs : int = 2 

53 
 "level of parallel proof checking: 0, 1, 2" 

51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51230
diff
changeset

54 
option parallel_subproofs_saturation : int = 100 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51230
diff
changeset

55 
 "upper bound for forks of nested proofs (multiplied by worker threads)" 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51230
diff
changeset

56 
option parallel_subproofs_threshold : real = 0.01 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51230
diff
changeset

57 
 "lower bound of timing estimate for forked nested proofs (seconds)" 
51230
19192615911e
option parallel_proofs_reuse_timing controls reuse of log information  since it is not always beneficial for performance;
wenzelm
parents:
51044
diff
changeset

58 
option parallel_proofs_reuse_timing : bool = true 
19192615911e
option parallel_proofs_reuse_timing controls reuse of log information  since it is not always beneficial for performance;
wenzelm
parents:
51044
diff
changeset

59 
 "reuse timing information from old log file for parallel proof scheduling" 
49270  60 

61 

49295  62 
section "Detail of Proof Recording" 
49270  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 

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

69 
 "skip over proofs (implicit 'sorry')" 
49270  70 

71 

49295  72 
section "Global Session Parameters" 
49270  73 

74 
option condition : string = "" 

75 
 "required environment variables for subsequent theories (separated by commas)" 

76 

48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

77 
option timing : bool = false 
48580  78 
 "global timing of toplevel command execution and theory processing" 
48492  79 

48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

80 
option timeout : real = 0 
48661  81 
 "timeout for session build job (seconds > 0)" 
82 

49288  83 

49295  84 
section "Editor Reactivity" 
49288  85 

51554
041bc3d31f23
separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
wenzelm
parents:
51553
diff
changeset

86 
option editor_skip_proofs : bool = false 
041bc3d31f23
separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
wenzelm
parents:
51553
diff
changeset

87 
 "skip over proofs (implicit 'sorry')" 
041bc3d31f23
separate option editor_skip_proofs, to avoid accidental change of preferences for skip_proofs, which would invalidate batch builds;
wenzelm
parents:
51553
diff
changeset

88 

49288  89 
option editor_load_delay : real = 0.5 
90 
 "delay for file load operations (new buffers etc.)" 

91 

92 
option editor_input_delay : real = 0.3 

93 
 "delay for user input (text edits, cursor movement etc.)" 

94 

95 
option editor_output_delay : real = 0.1 

96 
 "delay for prover output (markup, common messages etc.)" 

97 

98 
option editor_update_delay : real = 0.5 

99 
 "delay for physical GUI updates" 

100 

49524
68796a77c42b
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
wenzelm
parents:
49295
diff
changeset

101 
option editor_reparse_limit : int = 10000 
68796a77c42b
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
wenzelm
parents:
49295
diff
changeset

102 
 "maximum amount of reparsed text outside perspective" 
50119
5c370a036de7
more generous tracing_limit, with explicit system option;
wenzelm
parents:
49524
diff
changeset

103 

51044
890f502f0e89
more generous tracing limit, which is relevant for applications where this occurs routinely (e.g. HO unification trace);
wenzelm
parents:
50698
diff
changeset

104 
option editor_tracing_messages : int = 1000 
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50455
diff
changeset

105 
 "initial number of tracing messages for each command transaction" 
50697
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50505
diff
changeset

106 

82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50505
diff
changeset

107 
option editor_chart_delay : real = 3.0 
82e9178e6a98
improved Monitor_Dockable, based on ML_Statistics operations;
wenzelm
parents:
50505
diff
changeset

108 
 "delay for chart repainting" 