etc/options
changeset 49270 e5d162d15867
parent 48805 c3ea910b3581
child 49288 2c9272cb4568
     1.1 --- a/etc/options	Tue Sep 11 11:53:34 2012 +0200
     1.2 +++ b/etc/options	Tue Sep 11 15:47:42 2012 +0200
     1.3 @@ -1,5 +1,7 @@
     1.4  (* :mode=isabelle-options: *)
     1.5  
     1.6 +section {* Document preparation *}
     1.7 +
     1.8  option browser_info : bool = false
     1.9    -- "generate theory browser information"
    1.10  
    1.11 @@ -16,28 +18,6 @@
    1.12  option document_dump_mode : string = "all"
    1.13    -- "specific document dump mode: all, tex, tex+sty"
    1.14  
    1.15 -option threads : int = 0
    1.16 -  -- "maximum number of worker threads for prover process (0 = hardware max.)"
    1.17 -option threads_trace : int = 0
    1.18 -  -- "level of tracing information for multithreading"
    1.19 -option parallel_proofs : int = 2
    1.20 -  -- "level of parallel proof checking: 0, 1, 2"
    1.21 -option parallel_proofs_threshold : int = 100
    1.22 -  -- "threshold for sub-proof parallelization"
    1.23 -
    1.24 -option print_mode : string = ""
    1.25 -  -- "additional print modes for prover output (separated by commas)"
    1.26 -
    1.27 -option proofs : int = 1
    1.28 -  -- "level of detail for proof objects: 0, 1, 2"
    1.29 -option quick_and_dirty : bool = false
    1.30 -  -- "if true then some tools will OMIT some proofs"
    1.31 -option skip_proofs : bool = false
    1.32 -  -- "skip over proofs"
    1.33 -
    1.34 -option condition : string = ""
    1.35 -  -- "required environment variables for subsequent theories (separated by commas)"
    1.36 -
    1.37  option show_question_marks : bool = true
    1.38    -- "show leading question mark of schematic variables"
    1.39  
    1.40 @@ -62,6 +42,38 @@
    1.41  option thy_output_source : bool = false
    1.42    -- "print original source text rather than internal representation"
    1.43  
    1.44 +
    1.45 +option print_mode : string = ""
    1.46 +  -- "additional print modes for prover output (separated by commas)"
    1.47 +
    1.48 +
    1.49 +section {* Parallel checking *}
    1.50 +
    1.51 +option threads : int = 0
    1.52 +  -- "maximum number of worker threads for prover process (0 = hardware max.)"
    1.53 +option threads_trace : int = 0
    1.54 +  -- "level of tracing information for multithreading"
    1.55 +option parallel_proofs : int = 2
    1.56 +  -- "level of parallel proof checking: 0, 1, 2"
    1.57 +option parallel_proofs_threshold : int = 100
    1.58 +  -- "threshold for sub-proof parallelization"
    1.59 +
    1.60 +
    1.61 +section {* Detail of proof recording *}
    1.62 +
    1.63 +option proofs : int = 1
    1.64 +  -- "level of detail for proof objects: 0, 1, 2"
    1.65 +option quick_and_dirty : bool = false
    1.66 +  -- "if true then some tools will OMIT some proofs"
    1.67 +option skip_proofs : bool = false
    1.68 +  -- "skip over proofs"
    1.69 +
    1.70 +
    1.71 +section {* Global session parameters *}
    1.72 +
    1.73 +option condition : string = ""
    1.74 +  -- "required environment variables for subsequent theories (separated by commas)"
    1.75 +
    1.76  option timing : bool = false
    1.77    -- "global timing of toplevel command execution and theory processing"
    1.78