src/Pure/ProofGeneral/preferences.ML
author wenzelm
Fri Jun 13 21:04:42 2008 +0200 (2008-06-13)
changeset 27195 bbf4cbc69243
parent 25440 aa25d4d59383
child 28066 611e504c1191
permissions -rw-r--r--
map_const: soft version, no failure here;
aspinall@21637
     1
(*  Title:      Pure/ProofGeneral/preferences.ML
aspinall@21637
     2
    ID:         $Id$
aspinall@21637
     3
    Author:     David Aspinall and Markus Wenzel
aspinall@21637
     4
aspinall@21637
     5
User preferences for Isabelle which are maintained by the interface.
aspinall@21637
     6
*)
aspinall@21637
     7
wenzelm@24329
     8
signature PREFERENCES =
aspinall@21637
     9
sig
aspinall@21637
    10
  type pgiptype = PgipTypes.pgiptype
aspinall@21637
    11
aspinall@21637
    12
  type isa_preference = { name: string,
wenzelm@24329
    13
                          descr: string,
wenzelm@24329
    14
                          default: string,
wenzelm@24329
    15
                          pgiptype: pgiptype,
wenzelm@24329
    16
                          get: unit -> string,
wenzelm@24329
    17
                          set: string -> unit }
aspinall@21637
    18
aspinall@24191
    19
  (* table of categories and preferences; names must be unique *)
aspinall@22214
    20
  type isa_preference_table = (string * isa_preference list) list
aspinall@22214
    21
aspinall@22214
    22
  val preferences : isa_preference_table
aspinall@22214
    23
aspinall@22214
    24
  val remove      : string -> isa_preference_table -> isa_preference_table
aspinall@22214
    25
  val set_default : string * string -> isa_preference_table -> isa_preference_table
aspinall@21637
    26
end
aspinall@21637
    27
aspinall@21637
    28
structure Preferences : PREFERENCES =
aspinall@21637
    29
struct
aspinall@21637
    30
aspinall@21637
    31
val thm_depsN = "thm_deps";    (* also in proof_general_pgip.ML: move to pgip_isabelle? *)
aspinall@21637
    32
aspinall@21637
    33
type pgiptype = PgipTypes.pgiptype
aspinall@21637
    34
aspinall@21637
    35
type isa_preference = { name: string,
wenzelm@24329
    36
                        descr: string,
wenzelm@24329
    37
                        default: string,
wenzelm@24329
    38
                        pgiptype: pgiptype,
wenzelm@24329
    39
                        get: unit -> string,
wenzelm@24329
    40
                        set: string -> unit }
aspinall@21637
    41
aspinall@21637
    42
wenzelm@24329
    43
fun mkpref get set typ nm descr =
aspinall@21637
    44
    { name=nm, descr=descr, pgiptype=typ, get=get, set=set, default=get() } : isa_preference
aspinall@21637
    45
aspinall@21637
    46
fun mkpref_from_ref read write typ r nm descr =
aspinall@21637
    47
    mkpref (fn()=> read (!r)) (fn v=> r:= (write v)) typ nm descr
aspinall@21637
    48
wenzelm@24329
    49
val int_pref =
aspinall@21637
    50
    mkpref_from_ref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE,NONE))
wenzelm@24329
    51
                    (PgipTypes.Pgipint (NONE, NONE))
aspinall@21637
    52
val nat_pref =
aspinall@21637
    53
    mkpref_from_ref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat
aspinall@21637
    54
aspinall@21637
    55
val bool_pref =
aspinall@21637
    56
    mkpref_from_ref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool
aspinall@21637
    57
aspinall@21637
    58
val proof_pref =
wenzelm@24329
    59
    let
wenzelm@25223
    60
        fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2)
wenzelm@25223
    61
        fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1)
aspinall@21637
    62
    in
wenzelm@24329
    63
        mkpref get set PgipTypes.Pgipbool "full-proofs"
wenzelm@24329
    64
               "Record full proof objects internally"
aspinall@21637
    65
    end
aspinall@21637
    66
wenzelm@24329
    67
val thm_deps_pref =
wenzelm@24329
    68
    let
wenzelm@24329
    69
        fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN)
wenzelm@24614
    70
        fun set s =  NAMED_CRITICAL "print_mode" (fn () =>
wenzelm@24614
    71
          if PgipTypes.read_pgipbool s then
wenzelm@24614
    72
            change print_mode (insert (op =) thm_depsN)
wenzelm@24614
    73
          else
wenzelm@24614
    74
            change print_mode (remove (op =) thm_depsN))
aspinall@21637
    75
    in
wenzelm@24329
    76
        mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
wenzelm@24329
    77
               "Track theorem dependencies within Proof General"
aspinall@21637
    78
    end
aspinall@21637
    79
aspinall@21637
    80
val print_depth_pref =
wenzelm@24329
    81
    let
wenzelm@24329
    82
        fun get () = PgipTypes.int_to_pgstring (get_print_depth ())
wenzelm@24329
    83
        val set = print_depth o PgipTypes.read_pgipnat
aspinall@21637
    84
    in
wenzelm@24329
    85
        mkpref get set PgipTypes.Pgipnat
wenzelm@24329
    86
               "print-depth" "Setting for the ML print depth"
aspinall@21637
    87
    end
aspinall@21637
    88
aspinall@21637
    89
wenzelm@24329
    90
val display_preferences =
aspinall@21637
    91
    [bool_pref show_types
wenzelm@24329
    92
               "show-types"
wenzelm@24329
    93
               "Include types in display of Isabelle terms",
aspinall@21637
    94
     bool_pref show_sorts
wenzelm@24329
    95
               "show-sorts"
wenzelm@24329
    96
               "Include sorts in display of Isabelle terms",
aspinall@21637
    97
     bool_pref show_consts
wenzelm@24329
    98
               "show-consts"
wenzelm@24329
    99
               "Show types of consts in Isabelle goal display",
aspinall@21637
   100
     bool_pref long_names
wenzelm@24329
   101
               "long-names"
wenzelm@24329
   102
               "Show fully qualified names in Isabelle terms",
aspinall@21637
   103
     bool_pref show_brackets
wenzelm@24329
   104
               "show-brackets"
wenzelm@24329
   105
               "Show full bracketing in Isabelle terms",
aspinall@21637
   106
     bool_pref Proof.show_main_goal
wenzelm@24329
   107
               "show-main-goal"
wenzelm@24329
   108
               "Show main goal in proof state display",
aspinall@21637
   109
     bool_pref Syntax.eta_contract
wenzelm@24329
   110
               "eta-contract"
wenzelm@24329
   111
               "Print terms eta-contracted"]
aspinall@21637
   112
aspinall@21637
   113
val advanced_display_preferences =
aspinall@21637
   114
    [nat_pref goals_limit
wenzelm@24329
   115
              "goals-limit"
wenzelm@24329
   116
              "Setting for maximum number of goals printed",
aspinall@21637
   117
     int_pref ProofContext.prems_limit
wenzelm@24329
   118
              "prems-limit"
wenzelm@24329
   119
              "Setting for maximum number of premises printed",
wenzelm@24329
   120
     print_depth_pref,
aspinall@21637
   121
     bool_pref show_question_marks
wenzelm@24329
   122
               "show-question-marks"
wenzelm@24329
   123
               "Show leading question mark of variable name"]
aspinall@21637
   124
wenzelm@24329
   125
val tracing_preferences =
aspinall@21637
   126
    [bool_pref trace_simp
wenzelm@24329
   127
               "trace-simplifier"
wenzelm@24329
   128
               "Trace simplification rules.",
aspinall@21637
   129
     nat_pref trace_simp_depth_limit
wenzelm@24329
   130
              "trace-simplifier-depth"
wenzelm@24329
   131
              "Trace simplifier depth limit.",
aspinall@21637
   132
     bool_pref trace_rules
wenzelm@24329
   133
               "trace-rules"
wenzelm@24329
   134
               "Trace application of the standard rules",
aspinall@21637
   135
     bool_pref Pattern.trace_unify_fail
wenzelm@24329
   136
               "trace-unification"
wenzelm@24329
   137
               "Output error diagnostics during unification",
aspinall@21637
   138
     bool_pref Output.timing
wenzelm@24329
   139
               "global-timing"
wenzelm@24329
   140
               "Whether to enable timing in Isabelle.",
wenzelm@22130
   141
     bool_pref Toplevel.debug
wenzelm@24329
   142
                "debugging"
berghofe@24454
   143
                "Whether to enable debugging.",
berghofe@24454
   144
     bool_pref Codegen.auto_quickcheck
berghofe@24454
   145
                "auto-quickcheck"
wenzelm@24806
   146
                "Whether to enable quickcheck automatically.",
wenzelm@24806
   147
     nat_pref Codegen.auto_quickcheck_time_limit
wenzelm@24806
   148
                "auto-quickcheck-time-limit"
aspinall@25440
   149
                "Time limit for automatic quickcheck (in milliseconds).",
aspinall@25440
   150
     thm_deps_pref]
aspinall@21637
   151
wenzelm@24329
   152
val proof_preferences =
aspinall@21637
   153
    [bool_pref quick_and_dirty
wenzelm@24329
   154
               "quick-and-dirty"
wenzelm@24329
   155
               "Take a few short cuts",
aspinall@21637
   156
     bool_pref Toplevel.skip_proofs
wenzelm@24329
   157
               "skip-proofs"
wenzelm@24329
   158
               "Skip over proofs (interactive-only)",
berghofe@24454
   159
     proof_pref,
wenzelm@24100
   160
     nat_pref Multithreading.max_threads
wenzelm@24329
   161
               "max-threads"
wenzelm@24329
   162
               "Maximum number of threads"]
aspinall@21637
   163
wenzelm@24329
   164
val preferences =
aspinall@21637
   165
    [("Display", display_preferences),
aspinall@21637
   166
     ("Advanced Display", advanced_display_preferences),
aspinall@21637
   167
     ("Tracing", tracing_preferences),
aspinall@21637
   168
     ("Proof", proof_preferences)]
aspinall@21637
   169
aspinall@22214
   170
type isa_preference_table = (string * isa_preference list) list
aspinall@22214
   171
wenzelm@24329
   172
fun remove name (preftable : isa_preference_table)  =
wenzelm@24329
   173
    map (fn (cat,prefs) =>
wenzelm@24329
   174
            (cat, filter_out (curry op= name o #name) prefs))
aspinall@22214
   175
        preftable;
aspinall@22214
   176
wenzelm@24329
   177
fun set_default (setname,newdefault) (preftable : isa_preference_table)  =
wenzelm@24329
   178
    map (fn (cat,prefs) =>
wenzelm@24329
   179
            (cat, map (fn (pref as {name,descr,default,pgiptype,get,set})
wenzelm@24329
   180
                          => if (name = setname) then
wenzelm@24329
   181
                                 (set newdefault;
wenzelm@24329
   182
                                  {name=name,descr=descr,default=newdefault,
wenzelm@24329
   183
                                  pgiptype=pgiptype,get=get,set=set})
wenzelm@24329
   184
                             else pref)
wenzelm@24329
   185
                  prefs))
aspinall@22214
   186
        preftable;
aspinall@22214
   187
aspinall@21637
   188
end