author  wenzelm 
Thu, 16 May 2013 21:09:58 +0200  
changeset 52042  aae07a3ff536 
parent 51962  016cb7d8f297 
child 52043  286629271d65 
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 

51960
61ac1efe02c3
option "goals_limit", with more uniform description;
wenzelm
parents:
51564
diff
changeset

17 
option goals_limit : int = 10 
61ac1efe02c3
option "goals_limit", with more uniform description;
wenzelm
parents:
51564
diff
changeset

18 
 "maximum number of subgoals to be printed" 
61ac1efe02c3
option "goals_limit", with more uniform description;
wenzelm
parents:
51564
diff
changeset

19 

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

20 
option show_question_marks : bool = true 
48580  21 
 "show leading question mark of schematic variables" 
48486  22 

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

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

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

27 
option names_unique : bool = true 
48580  28 
 "show partially qualified names, as required for unique name resolution" 
48486  29 

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

30 
option pretty_margin : int = 76 
48580  31 
 "right margin / page width of pretty printer in Isabelle/ML" 
48527  32 

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

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

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

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

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

41 
option thy_output_source : bool = false 
48580  42 
 "print original source text rather than internal representation" 
52042  43 
option thy_output_modes : string = "" 
44 
 "additional print modes for document output (separated by commas)" 

49270  45 

46 
option print_mode : string = "" 

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

48 

49 

49295  50 
section "Parallel Checking" 
49270  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" 

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

58 
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

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

60 
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

61 
 "lower bound of timing estimate for forked nested proofs (seconds)" 
49270  62 

63 

49295  64 
section "Detail of Proof Recording" 
49270  65 

66 
option proofs : int = 1 

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

68 
option quick_and_dirty : bool = false 

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

70 
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

71 
 "skip over proofs (implicit 'sorry')" 
49270  72 

73 

49295  74 
section "Global Session Parameters" 
49270  75 

76 
option condition : string = "" 

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

78 

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

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

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

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

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

85 
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

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

87 

49288  88 

49295  89 
section "Editor Reactivity" 
49288  90 

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

91 
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

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

93 

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

96 

97 
option editor_input_delay : real = 0.3 

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

99 

100 
option editor_output_delay : real = 0.1 

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

102 

103 
option editor_update_delay : real = 0.5 

104 
 "delay for physical GUI updates" 

105 

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

106 
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

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

108 

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

109 
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

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

111 

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

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

113 
 "delay for chart repainting" 