etc/options
changeset 48795 bece259ee055
parent 48661 9149ebdd0241
child 48805 c3ea910b3581
     1.1 --- a/etc/options	Tue Aug 14 12:26:02 2012 +0200
     1.2 +++ b/etc/options	Tue Aug 14 13:01:09 2012 +0200
     1.3 @@ -1,68 +1,68 @@
     1.4  (* :mode=isabelle-options: *)
     1.5  
     1.6 -declare browser_info : bool = false
     1.7 +option browser_info : bool = false
     1.8    -- "generate theory browser information"
     1.9  
    1.10 -declare document : string = ""
    1.11 +option document : string = ""
    1.12    -- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
    1.13 -declare document_variants : string = "outline=/proof,/ML"
    1.14 -  -- "declare alternative document variants (separated by colons)"
    1.15 -declare document_graph : bool = false
    1.16 +option document_variants : string = "outline=/proof,/ML"
    1.17 +  -- "option alternative document variants (separated by colons)"
    1.18 +option document_graph : bool = false
    1.19    -- "generate session graph image for document"
    1.20 -declare document_dump : string = ""
    1.21 +option document_dump : string = ""
    1.22    -- "dump generated document sources into given directory"
    1.23 -declare document_dump_mode : string = "all"
    1.24 +option document_dump_mode : string = "all"
    1.25    -- "specific document dump mode: all, tex, tex+sty"
    1.26  
    1.27 -declare threads : int = 0
    1.28 +option threads : int = 0
    1.29    -- "maximum number of worker threads for prover process (0 = hardware max.)"
    1.30 -declare threads_trace : int = 0
    1.31 +option threads_trace : int = 0
    1.32    -- "level of tracing information for multithreading"
    1.33 -declare parallel_proofs : int = 2
    1.34 +option parallel_proofs : int = 2
    1.35    -- "level of parallel proof checking: 0, 1, 2"
    1.36 -declare parallel_proofs_threshold : int = 100
    1.37 +option parallel_proofs_threshold : int = 100
    1.38    -- "threshold for sub-proof parallelization"
    1.39  
    1.40 -declare print_mode : string = ""
    1.41 +option print_mode : string = ""
    1.42    -- "additional print modes for prover output (separated by commas)"
    1.43  
    1.44 -declare proofs : int = 1
    1.45 +option proofs : int = 1
    1.46    -- "level of detail for proof objects: 0, 1, 2"
    1.47 -declare quick_and_dirty : bool = false
    1.48 +option quick_and_dirty : bool = false
    1.49    -- "if true then some tools will OMIT some proofs"
    1.50 -declare skip_proofs : bool = false
    1.51 +option skip_proofs : bool = false
    1.52    -- "skip over proofs"
    1.53  
    1.54 -declare condition : string = ""
    1.55 +option condition : string = ""
    1.56    -- "required environment variables for subsequent theories (separated by commas)"
    1.57  
    1.58 -declare show_question_marks : bool = true
    1.59 +option show_question_marks : bool = true
    1.60    -- "show leading question mark of schematic variables"
    1.61  
    1.62 -declare names_long : bool = false
    1.63 +option names_long : bool = false
    1.64    -- "show fully qualified names"
    1.65 -declare names_short : bool = false
    1.66 +option names_short : bool = false
    1.67    -- "show base names only"
    1.68 -declare names_unique : bool = true
    1.69 +option names_unique : bool = true
    1.70    -- "show partially qualified names, as required for unique name resolution"
    1.71  
    1.72 -declare pretty_margin : int = 76
    1.73 +option pretty_margin : int = 76
    1.74    -- "right margin / page width of pretty printer in Isabelle/ML"
    1.75  
    1.76 -declare thy_output_display : bool = false
    1.77 +option thy_output_display : bool = false
    1.78    -- "indicate output as multi-line display-style material"
    1.79 -declare thy_output_break : bool = false
    1.80 +option thy_output_break : bool = false
    1.81    -- "control line breaks in non-display material"
    1.82 -declare thy_output_quotes : bool = false
    1.83 +option thy_output_quotes : bool = false
    1.84    -- "indicate if the output should be enclosed in double quotes"
    1.85 -declare thy_output_indent : int = 0
    1.86 +option thy_output_indent : int = 0
    1.87    -- "indentation for pretty printing of display material"
    1.88 -declare thy_output_source : bool = false
    1.89 +option thy_output_source : bool = false
    1.90    -- "print original source text rather than internal representation"
    1.91  
    1.92 -declare timing : bool = false
    1.93 +option timing : bool = false
    1.94    -- "global timing of toplevel command execution and theory processing"
    1.95  
    1.96 -declare timeout : real = 0
    1.97 +option timeout : real = 0
    1.98    -- "timeout for session build job (seconds > 0)"
    1.99