etc/options
changeset 52043 286629271d65
parent 52042 aae07a3ff536
child 52065 78f2475aa126
     1.1 --- a/etc/options	Thu May 16 21:09:58 2013 +0200
     1.2 +++ b/etc/options	Thu May 16 21:48:01 2013 +0200
     1.3 @@ -14,22 +14,6 @@
     1.4  option document_graph : bool = false
     1.5    -- "generate session graph image for document"
     1.6  
     1.7 -option goals_limit : int = 10
     1.8 -  -- "maximum number of subgoals to be printed"
     1.9 -
    1.10 -option show_question_marks : bool = true
    1.11 -  -- "show leading question mark of schematic variables"
    1.12 -
    1.13 -option names_long : bool = false
    1.14 -  -- "show fully qualified names"
    1.15 -option names_short : bool = false
    1.16 -  -- "show base names only"
    1.17 -option names_unique : bool = true
    1.18 -  -- "show partially qualified names, as required for unique name resolution"
    1.19 -
    1.20 -option pretty_margin : int = 76
    1.21 -  -- "right margin / page width of pretty printer in Isabelle/ML"
    1.22 -
    1.23  option thy_output_display : bool = false
    1.24    -- "indicate output as multi-line display-style material"
    1.25  option thy_output_break : bool = false
    1.26 @@ -43,6 +27,38 @@
    1.27  option thy_output_modes : string = ""
    1.28    -- "additional print modes for document output (separated by commas)"
    1.29  
    1.30 +
    1.31 +section "Prover Output"
    1.32 +
    1.33 +option show_types : bool = false
    1.34 +  -- "show type constraints when printing terms"
    1.35 +option show_sorts : bool = false
    1.36 +  -- "show sort constraints when printing types"
    1.37 +option show_brackets : bool = false
    1.38 +  -- "show extra brackets when printing terms/types"
    1.39 +option show_question_marks : bool = true
    1.40 +  -- "show leading question mark of schematic variables"
    1.41 +
    1.42 +option show_consts : bool = false
    1.43 +  -- "show constants with types when printing proof state"
    1.44 +option show_main_goal : bool = false
    1.45 +  -- "show main goal when printing proof state"
    1.46 +option goals_limit : int = 10
    1.47 +  -- "maximum number of subgoals to be printed"
    1.48 +
    1.49 +option names_long : bool = false
    1.50 +  -- "show fully qualified names"
    1.51 +option names_short : bool = false
    1.52 +  -- "show base names only"
    1.53 +option names_unique : bool = true
    1.54 +  -- "show partially qualified names, as required for unique name resolution"
    1.55 +
    1.56 +option eta_contract : bool = true
    1.57 +  -- "print terms in eta-contracted form"
    1.58 +
    1.59 +option pretty_margin : int = 76
    1.60 +  -- "right margin / page width of pretty printer in Isabelle/ML"
    1.61 +
    1.62  option print_mode : string = ""
    1.63    -- "additional print modes for prover output (separated by commas)"
    1.64