etc/options
changeset 48580 9df76dd45900
parent 48527 4ee8d70cd5a3
child 48634 30a6e841390a
     1.1 --- a/etc/options	Sat Jul 28 18:20:47 2012 +0200
     1.2 +++ b/etc/options	Sat Jul 28 19:37:35 2012 +0200
     1.3 @@ -1,39 +1,63 @@
     1.4  (* :mode=isabelle-options: *)
     1.5  
     1.6  declare browser_info : bool = false
     1.7 +  -- "generate theory browser information"
     1.8  
     1.9  declare document : string = ""
    1.10 +  -- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
    1.11  declare document_variants : string = "outline=/proof,/ML"
    1.12 +  -- "declare alternative document variants (separated by colons)"
    1.13  declare document_graph : bool = false
    1.14 +  -- "generate session graph image for document"
    1.15  declare document_dump : string = ""
    1.16 +  -- "dump generated document sources into given directory"
    1.17  declare document_dump_mode : string = "all"
    1.18 -declare no_document : bool = false
    1.19 +  -- "specific document dump mode: all, tex, tex+sty"
    1.20  
    1.21  declare threads : int = 0
    1.22 +  -- "maximum number of worker threads for prover process (0 = hardware max.)"
    1.23  declare threads_trace : int = 0
    1.24 +  -- "level of tracing information for multithreading"
    1.25  declare parallel_proofs : int = 2
    1.26 +  -- "level of parallel proof checking: 0, 1, 2"
    1.27  declare parallel_proofs_threshold : int = 100
    1.28 +  -- "threshold for sub-proof parallelization"
    1.29  
    1.30  declare print_mode : string = ""
    1.31 +  -- "additional print modes for prover output (separated by commas)"
    1.32  
    1.33  declare proofs : int = 1
    1.34 +  -- "level of detail for proof objects: 0, 1, 2"
    1.35  declare quick_and_dirty : bool = false
    1.36 +  -- "if true then some tools will OMIT some proofs"
    1.37  
    1.38  declare condition : string = ""
    1.39 +  -- "required environment variables for subsequent theories (separated by commas)"
    1.40  
    1.41  declare show_question_marks : bool = true
    1.42 +  -- "show leading question mark of schematic variables"
    1.43  
    1.44  declare names_long : bool = false
    1.45 +  -- "show fully qualified names"
    1.46  declare names_short : bool = false
    1.47 +  -- "show base names only"
    1.48  declare names_unique : bool = true
    1.49 +  -- "show partially qualified names, as required for unique name resolution"
    1.50  
    1.51  declare pretty_margin : int = 76
    1.52 +  -- "right margin / page width of pretty printer in Isabelle/ML"
    1.53  
    1.54  declare thy_output_display : bool = false
    1.55 +  -- "indicate output as multi-line display-style material"
    1.56 +declare thy_output_break : bool = false
    1.57 +  -- "control line breaks in non-display material"
    1.58  declare thy_output_quotes : bool = false
    1.59 +  -- "indicate if the output should be enclosed in double quotes"
    1.60  declare thy_output_indent : int = 0
    1.61 +  -- "indentation for pretty printing of display material"
    1.62  declare thy_output_source : bool = false
    1.63 -declare thy_output_break : bool = false
    1.64 +  -- "print original source text rather than internal representation"
    1.65  
    1.66  declare timing : bool = false
    1.67 +  -- "global timing of toplevel command execution and theory processing"
    1.68