author  wenzelm 
Thu, 16 May 2013 21:48:01 +0200  
changeset 52043  286629271d65 
parent 52042  aae07a3ff536 
child 52065  78f2475aa126 
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 thy_output_display : bool = false 
48580  18 
 "indicate output as multiline displaystyle material" 
48795
bece259ee055
clarified format of etc/options: only declarations, not redefinitions;
wenzelm
parents:
48661
diff
changeset

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

21 
option thy_output_quotes : bool = false 
48580  22 
 "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

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

25 
option thy_output_source : bool = false 
48580  26 
 "print original source text rather than internal representation" 
52042  27 
option thy_output_modes : string = "" 
28 
 "additional print modes for document output (separated by commas)" 

49270  29 

52043
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

30 

286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

31 
section "Prover Output" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

32 

286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

33 
option show_types : bool = false 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

34 
 "show type constraints when printing terms" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

35 
option show_sorts : bool = false 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

36 
 "show sort constraints when printing types" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

37 
option show_brackets : bool = false 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

38 
 "show extra brackets when printing terms/types" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

39 
option show_question_marks : bool = true 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

40 
 "show leading question mark of schematic variables" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

41 

286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

42 
option show_consts : bool = false 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

43 
 "show constants with types when printing proof state" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

44 
option show_main_goal : bool = false 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

45 
 "show main goal when printing proof state" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

46 
option goals_limit : int = 10 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

47 
 "maximum number of subgoals to be printed" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

48 

286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

49 
option names_long : bool = false 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

50 
 "show fully qualified names" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

51 
option names_short : bool = false 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

52 
 "show base names only" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

53 
option names_unique : bool = true 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

54 
 "show partially qualified names, as required for unique name resolution" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

55 

286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

56 
option eta_contract : bool = true 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

57 
 "print terms in etacontracted form" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

58 

286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

59 
option pretty_margin : int = 76 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

60 
 "right margin / page width of pretty printer in Isabelle/ML" 
286629271d65
more system options as contextsensitive config options;
wenzelm
parents:
52042
diff
changeset

61 

49270  62 
option print_mode : string = "" 
63 
 "additional print modes for prover output (separated by commas)" 

64 

65 

49295  66 
section "Parallel Checking" 
49270  67 

68 
option threads : int = 0 

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

70 
option threads_trace : int = 0 

71 
 "level of tracing information for multithreading" 

72 
option parallel_proofs : int = 2 

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

74 
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

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

76 
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

77 
 "lower bound of timing estimate for forked nested proofs (seconds)" 
49270  78 

79 

49295  80 
section "Detail of Proof Recording" 
49270  81 

82 
option proofs : int = 1 

83 
 "level of detail for proof objects: 0, 1, 2" 

84 
option quick_and_dirty : bool = false 

85 
 "if true then some tools will OMIT some proofs" 

86 
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

87 
 "skip over proofs (implicit 'sorry')" 
49270  88 

89 

49295  90 
section "Global Session Parameters" 
49270  91 

92 
option condition : string = "" 

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

94 

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

95 
option timing : bool = false 
48580  96 
 "global timing of toplevel command execution and theory processing" 
48492  97 

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

98 
option timeout : real = 0 
48661  99 
 "timeout for session build job (seconds > 0)" 
100 

51962
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51960
diff
changeset

101 
option process_output_limit : int = 100 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51960
diff
changeset

102 
 "build process output limit in million characters (0 = unlimited)" 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51960
diff
changeset

103 

49288  104 

49295  105 
section "Editor Reactivity" 
49288  106 

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

107 
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

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

109 

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

112 

113 
option editor_input_delay : real = 0.3 

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

115 

116 
option editor_output_delay : real = 0.1 

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

118 

119 
option editor_update_delay : real = 0.5 

120 
 "delay for physical GUI updates" 

121 

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

122 
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

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

124 

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

125 
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

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

127 

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

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

129 
 "delay for chart repainting" 