wenzelm@48367: (* :mode=isabelle-options: *)
wenzelm@48367: 
wenzelm@49295: section "Document Preparation"
wenzelm@49270: 
wenzelm@48795: option browser_info : bool = false
wenzelm@48580:   -- "generate theory browser information"
wenzelm@48367: 
wenzelm@48795: option document : string = ""
wenzelm@48580:   -- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
wenzelm@48805: option document_output : string = ""
wenzelm@48805:   -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
wenzelm@48805: option document_variants : string = "document"
wenzelm@48795:   -- "option alternative document variants (separated by colons)"
wenzelm@48795: option document_graph : bool = false
wenzelm@48580:   -- "generate session graph image for document"
wenzelm@48367: 
wenzelm@48795: option show_question_marks : bool = true
wenzelm@48580:   -- "show leading question mark of schematic variables"
wenzelm@48486: 
wenzelm@48795: option names_long : bool = false
wenzelm@48580:   -- "show fully qualified names"
wenzelm@48795: option names_short : bool = false
wenzelm@48580:   -- "show base names only"
wenzelm@48795: option names_unique : bool = true
wenzelm@48580:   -- "show partially qualified names, as required for unique name resolution"
wenzelm@48486: 
wenzelm@48795: option pretty_margin : int = 76
wenzelm@48580:   -- "right margin / page width of pretty printer in Isabelle/ML"
wenzelm@48527: 
wenzelm@48795: option thy_output_display : bool = false
wenzelm@48580:   -- "indicate output as multi-line display-style material"
wenzelm@48795: option thy_output_break : bool = false
wenzelm@48580:   -- "control line breaks in non-display material"
wenzelm@48795: option thy_output_quotes : bool = false
wenzelm@48580:   -- "indicate if the output should be enclosed in double quotes"
wenzelm@48795: option thy_output_indent : int = 0
wenzelm@48580:   -- "indentation for pretty printing of display material"
wenzelm@48795: option thy_output_source : bool = false
wenzelm@48580:   -- "print original source text rather than internal representation"
wenzelm@48520: 
wenzelm@49270: 
wenzelm@49270: option print_mode : string = ""
wenzelm@49270:   -- "additional print modes for prover output (separated by commas)"
wenzelm@49270: 
wenzelm@49270: 
wenzelm@49295: section "Parallel Checking"
wenzelm@49270: 
wenzelm@49270: option threads : int = 0
wenzelm@49270:   -- "maximum number of worker threads for prover process (0 = hardware max.)"
wenzelm@49270: option threads_trace : int = 0
wenzelm@49270:   -- "level of tracing information for multithreading"
wenzelm@49270: option parallel_proofs : int = 2
wenzelm@49270:   -- "level of parallel proof checking: 0, 1, 2"
wenzelm@51423: option parallel_subproofs_saturation : int = 100
wenzelm@51423:   -- "upper bound for forks of nested proofs (multiplied by worker threads)"
wenzelm@51423: option parallel_subproofs_threshold : real = 0.01
wenzelm@51423:   -- "lower bound of timing estimate for forked nested proofs (seconds)"
wenzelm@51230: option parallel_proofs_reuse_timing : bool = true
wenzelm@51230:   -- "reuse timing information from old log file for parallel proof scheduling"
wenzelm@49270: 
wenzelm@49270: 
wenzelm@49295: section "Detail of Proof Recording"
wenzelm@49270: 
wenzelm@49270: option proofs : int = 1
wenzelm@49270:   -- "level of detail for proof objects: 0, 1, 2"
wenzelm@49270: option quick_and_dirty : bool = false
wenzelm@49270:   -- "if true then some tools will OMIT some proofs"
wenzelm@49270: option skip_proofs : bool = false
wenzelm@49270:   -- "skip over proofs"
wenzelm@49270: 
wenzelm@49270: 
wenzelm@49295: section "Global Session Parameters"
wenzelm@49270: 
wenzelm@49270: option condition : string = ""
wenzelm@49270:   -- "required environment variables for subsequent theories (separated by commas)"
wenzelm@49270: 
wenzelm@48795: option timing : bool = false
wenzelm@48580:   -- "global timing of toplevel command execution and theory processing"
wenzelm@48492: 
wenzelm@48795: option timeout : real = 0
wenzelm@48661:   -- "timeout for session build job (seconds > 0)"
wenzelm@48661: 
wenzelm@49288: 
wenzelm@49295: section "Editor Reactivity"
wenzelm@49288: 
wenzelm@49288: option editor_load_delay : real = 0.5
wenzelm@49288:   -- "delay for file load operations (new buffers etc.)"
wenzelm@49288: 
wenzelm@49288: option editor_input_delay : real = 0.3
wenzelm@49288:   -- "delay for user input (text edits, cursor movement etc.)"
wenzelm@49288: 
wenzelm@49288: option editor_output_delay : real = 0.1
wenzelm@49288:   -- "delay for prover output (markup, common messages etc.)"
wenzelm@49288: 
wenzelm@49288: option editor_update_delay : real = 0.5
wenzelm@49288:   -- "delay for physical GUI updates"
wenzelm@49288: 
wenzelm@49524: option editor_reparse_limit : int = 10000
wenzelm@49524:   -- "maximum amount of reparsed text outside perspective"
wenzelm@50119: 
wenzelm@51044: option editor_tracing_messages : int = 1000
wenzelm@50505:   -- "initial number of tracing messages for each command transaction"
wenzelm@50697: 
wenzelm@50697: option editor_chart_delay : real = 3.0
wenzelm@50697:   -- "delay for chart repainting"