etc/options
author wenzelm
Wed, 01 Aug 2012 15:46:45 +0200
changeset 48634 30a6e841390a
parent 48580 9df76dd45900
child 48661 9149ebdd0241
permissions -rw-r--r--
explicit option skip_proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48367
680d297ec71b some basic Isabelle options;
wenzelm
parents:
diff changeset
     1
(* :mode=isabelle-options: *)
680d297ec71b some basic Isabelle options;
wenzelm
parents:
diff changeset
     2
48370
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 48367
diff changeset
     3
declare browser_info : bool = false
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
     4
  -- "generate theory browser information"
48367
680d297ec71b some basic Isabelle options;
wenzelm
parents:
diff changeset
     5
48458
09710d6fc3d1 clarified document options;
wenzelm
parents: 48457
diff changeset
     6
declare document : string = ""
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
     7
  -- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
48466
3b2fb20df17d further imitation of ISABELLE_USEDIR_OPTIONS via options;
wenzelm
parents: 48463
diff changeset
     8
declare document_variants : string = "outline=/proof,/ML"
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
     9
  -- "declare alternative document variants (separated by colons)"
48370
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 48367
diff changeset
    10
declare document_graph : bool = false
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    11
  -- "generate session graph image for document"
48457
fd9e28d5a143 pass build options to ML;
wenzelm
parents: 48370
diff changeset
    12
declare document_dump : string = ""
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    13
  -- "dump generated document sources into given directory"
48516
c5d0f19ef7cb refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents: 48513
diff changeset
    14
declare document_dump_mode : string = "all"
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    15
  -- "specific document dump mode: all, tex, tex+sty"
48367
680d297ec71b some basic Isabelle options;
wenzelm
parents:
diff changeset
    16
48466
3b2fb20df17d further imitation of ISABELLE_USEDIR_OPTIONS via options;
wenzelm
parents: 48463
diff changeset
    17
declare threads : int = 0
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    18
  -- "maximum number of worker threads for prover process (0 = hardware max.)"
48370
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 48367
diff changeset
    19
declare threads_trace : int = 0
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    20
  -- "level of tracing information for multithreading"
48466
3b2fb20df17d further imitation of ISABELLE_USEDIR_OPTIONS via options;
wenzelm
parents: 48463
diff changeset
    21
declare parallel_proofs : int = 2
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    22
  -- "level of parallel proof checking: 0, 1, 2"
48370
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 48367
diff changeset
    23
declare parallel_proofs_threshold : int = 100
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    24
  -- "threshold for sub-proof parallelization"
48367
680d297ec71b some basic Isabelle options;
wenzelm
parents:
diff changeset
    25
48370
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 48367
diff changeset
    26
declare print_mode : string = ""
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    27
  -- "additional print modes for prover output (separated by commas)"
48367
680d297ec71b some basic Isabelle options;
wenzelm
parents:
diff changeset
    28
48466
3b2fb20df17d further imitation of ISABELLE_USEDIR_OPTIONS via options;
wenzelm
parents: 48463
diff changeset
    29
declare proofs : int = 1
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    30
  -- "level of detail for proof objects: 0, 1, 2"
48370
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 48367
diff changeset
    31
declare quick_and_dirty : bool = false
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    32
  -- "if true then some tools will OMIT some proofs"
48634
30a6e841390a explicit option skip_proofs;
wenzelm
parents: 48580
diff changeset
    33
declare skip_proofs : bool = false
30a6e841390a explicit option skip_proofs;
wenzelm
parents: 48580
diff changeset
    34
  -- "skip over proofs"
48367
680d297ec71b some basic Isabelle options;
wenzelm
parents:
diff changeset
    35
48370
d0fa3efec93b require explicit initialization of options;
wenzelm
parents: 48367
diff changeset
    36
declare condition : string = ""
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    37
  -- "required environment variables for subsequent theories (separated by commas)"
48367
680d297ec71b some basic Isabelle options;
wenzelm
parents:
diff changeset
    38
48486
691d0b44a793 more build options;
wenzelm
parents: 48468
diff changeset
    39
declare show_question_marks : bool = true
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    40
  -- "show leading question mark of schematic variables"
48486
691d0b44a793 more build options;
wenzelm
parents: 48468
diff changeset
    41
691d0b44a793 more build options;
wenzelm
parents: 48468
diff changeset
    42
declare names_long : bool = false
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    43
  -- "show fully qualified names"
48486
691d0b44a793 more build options;
wenzelm
parents: 48468
diff changeset
    44
declare names_short : bool = false
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    45
  -- "show base names only"
48486
691d0b44a793 more build options;
wenzelm
parents: 48468
diff changeset
    46
declare names_unique : bool = true
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    47
  -- "show partially qualified names, as required for unique name resolution"
48486
691d0b44a793 more build options;
wenzelm
parents: 48468
diff changeset
    48
48527
4ee8d70cd5a3 more build options;
wenzelm
parents: 48520
diff changeset
    49
declare pretty_margin : int = 76
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    50
  -- "right margin / page width of pretty printer in Isabelle/ML"
48527
4ee8d70cd5a3 more build options;
wenzelm
parents: 48520
diff changeset
    51
48520
6d4ea2efa64b more build options;
wenzelm
parents: 48516
diff changeset
    52
declare thy_output_display : bool = false
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    53
  -- "indicate output as multi-line display-style material"
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    54
declare thy_output_break : bool = false
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    55
  -- "control line breaks in non-display material"
48520
6d4ea2efa64b more build options;
wenzelm
parents: 48516
diff changeset
    56
declare thy_output_quotes : bool = false
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    57
  -- "indicate if the output should be enclosed in double quotes"
48520
6d4ea2efa64b more build options;
wenzelm
parents: 48516
diff changeset
    58
declare thy_output_indent : int = 0
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    59
  -- "indentation for pretty printing of display material"
48520
6d4ea2efa64b more build options;
wenzelm
parents: 48516
diff changeset
    60
declare thy_output_source : bool = false
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    61
  -- "print original source text rather than internal representation"
48520
6d4ea2efa64b more build options;
wenzelm
parents: 48516
diff changeset
    62
48492
03530cf284ca more build options;
wenzelm
parents: 48486
diff changeset
    63
declare timing : bool = false
48580
9df76dd45900 some description of main build options;
wenzelm
parents: 48527
diff changeset
    64
  -- "global timing of toplevel command execution and theory processing"
48492
03530cf284ca more build options;
wenzelm
parents: 48486
diff changeset
    65