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@52746: -- "build document in given format: pdf, dvi, 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@48367: 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@59175: option thy_output_margin : int = 76 wenzelm@59175: -- "right margin / page width for printing of display material" 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@52042: option thy_output_modes : string = "" wenzelm@52042: -- "additional print modes for document output (separated by commas)" wenzelm@49270: wenzelm@52043: wenzelm@52043: section "Prover Output" wenzelm@52043: wenzelm@52043: option show_types : bool = false wenzelm@52043: -- "show type constraints when printing terms" wenzelm@52043: option show_sorts : bool = false wenzelm@52043: -- "show sort constraints when printing types" wenzelm@52043: option show_brackets : bool = false wenzelm@52043: -- "show extra brackets when printing terms/types" wenzelm@52043: option show_question_marks : bool = true wenzelm@52043: -- "show leading question mark of schematic variables" wenzelm@52043: wenzelm@52043: option show_consts : bool = false wenzelm@52043: -- "show constants with types when printing proof state" wenzelm@52043: option show_main_goal : bool = false wenzelm@52043: -- "show main goal when printing proof state" wenzelm@52043: option goals_limit : int = 10 wenzelm@52043: -- "maximum number of subgoals to be printed" wenzelm@52043: wenzelm@52043: option names_long : bool = false wenzelm@52043: -- "show fully qualified names" wenzelm@52043: option names_short : bool = false wenzelm@52043: -- "show base names only" wenzelm@52043: option names_unique : bool = true wenzelm@52043: -- "show partially qualified names, as required for unique name resolution" wenzelm@52043: wenzelm@52043: option eta_contract : bool = true wenzelm@52043: -- "print terms in eta-contracted form" wenzelm@52043: wenzelm@49270: option print_mode : string = "" wenzelm@49270: -- "additional print modes for prover output (separated by commas)" wenzelm@49270: wenzelm@49270: wenzelm@56875: section "Parallel Processing" wenzelm@49270: wenzelm@52065: public option threads : int = 0 wenzelm@49270: -- "maximum number of worker threads for prover process (0 = hardware max.)" wenzelm@56734: option threads_trace : int = 0 wenzelm@49270: -- "level of tracing information for multithreading" wenzelm@59468: option threads_stack_limit : real = 0.25 wenzelm@59468: -- "maximum stack size for worker threads (in giga words, 0 = unlimited)" wenzelm@56875: public option parallel_print : bool = true wenzelm@56875: -- "parallel and asynchronous printing of results" wenzelm@52065: public option parallel_proofs : int = 2 wenzelm@49270: -- "level of parallel proof checking: 0, 1, 2" wenzelm@52714: option parallel_subproofs_threshold : real = 0.01 wenzelm@51423: -- "lower bound of timing estimate for forked nested proofs (seconds)" wenzelm@49270: wenzelm@49270: wenzelm@52490: section "Detail of Proof Checking" wenzelm@49270: 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@51553: -- "skip over proofs (implicit 'sorry')" 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 timeout : real = 0 wenzelm@48661: -- "timeout for session build job (seconds > 0)" wenzelm@48661: wenzelm@51962: option process_output_limit : int = 100 wenzelm@51962: -- "build process output limit in million characters (0 = unlimited)" wenzelm@51962: wenzelm@56279: wenzelm@56279: section "ML System" wenzelm@56279: wenzelm@56279: public option ML_exception_trace : bool = false wenzelm@56279: -- "ML exception trace for toplevel command execution" wenzelm@56265: wenzelm@60730: public option ML_debugger : bool = false wenzelm@60730: -- "ML debugger instrumentation for newly compiled code" wenzelm@60730: wenzelm@60074: public option ML_statistics : bool = true wenzelm@60843: -- "ML run-time system statistics" wenzelm@60074: wenzelm@61158: public option ML_system_64 : bool = false wenzelm@61158: -- "ML system for 64bit platform is used if possible (change requires restart)" wenzelm@61158: wenzelm@49288: wenzelm@49295: section "Editor Reactivity" wenzelm@49288: wenzelm@52065: public option editor_load_delay : real = 0.5 wenzelm@49288: -- "delay for file load operations (new buffers etc.)" wenzelm@49288: wenzelm@52065: public option editor_input_delay : real = 0.3 wenzelm@49288: -- "delay for user input (text edits, cursor movement etc.)" wenzelm@49288: wenzelm@52065: public option editor_output_delay : real = 0.1 wenzelm@49288: -- "delay for prover output (markup, common messages etc.)" wenzelm@49288: wenzelm@57867: public option editor_prune_delay : real = 60.0 wenzelm@57867: -- "delay to prune history (delete old versions)" wenzelm@57867: wenzelm@52065: public option editor_update_delay : real = 0.5 wenzelm@49288: -- "delay for physical GUI updates" wenzelm@49288: wenzelm@52065: public option editor_reparse_limit : int = 10000 wenzelm@49524: -- "maximum amount of reparsed text outside perspective" wenzelm@50119: wenzelm@52065: public option editor_tracing_messages : int = 1000 wenzelm@50505: -- "initial number of tracing messages for each command transaction" wenzelm@50697: wenzelm@52065: public option editor_chart_delay : real = 3.0 wenzelm@50697: -- "delay for chart repainting" wenzelm@52702: wenzelm@52807: public option editor_continuous_checking : bool = true wenzelm@52807: -- "continuous checking of proof document (visible and required parts)" wenzelm@52807: wenzelm@61213: public option editor_output_state : bool = true wenzelm@61213: -- "implicit output of proof state" wenzelm@61213: wenzelm@52798: option editor_execution_delay : real = 0.02 wenzelm@52798: -- "delay for start of execution process after document update (seconds)" wenzelm@52798: wenzelm@57974: option editor_syslog_limit : int = 100 wenzelm@57974: -- "maximum amount of buffered syslog messages" wenzelm@57974: wenzelm@52702: wenzelm@52702: section "Miscellaneous Tools" wenzelm@52702: wenzelm@52702: public option find_theorems_limit : int = 40 wenzelm@52702: -- "limit of displayed results" wenzelm@52702: wenzelm@56613: public option find_theorems_tactic_limit : int = 5 wenzelm@52702: -- "limit of tactic search for 'solves' criterion" wenzelm@52702: wenzelm@55672: wenzelm@55672: section "Completion" wenzelm@55672: wenzelm@55672: public option completion_limit : int = 40 wenzelm@55672: -- "limit for completion within the formal context" wenzelm@55672: