author wenzelm
Mon, 01 Oct 2007 21:19:54 +0200
changeset 24806 c070cd2a1450
parent 24614 a4b2eb0dd673
child 25223 7463251e7273
permissions -rw-r--r--
added auto-quickcheck-time-limit;

(*  Title:      Pure/ProofGeneral/preferences.ML
    ID:         $Id$
    Author:     David Aspinall and Markus Wenzel

User preferences for Isabelle which are maintained by the interface.

signature PREFERENCES =
  type pgiptype = PgipTypes.pgiptype

  type isa_preference = { name: string,
                          descr: string,
                          default: string,
                          pgiptype: pgiptype,
                          get: unit -> string,
                          set: string -> unit }

  (* table of categories and preferences; names must be unique *)
  type isa_preference_table = (string * isa_preference list) list

  val preferences : isa_preference_table

  val remove      : string -> isa_preference_table -> isa_preference_table
  val set_default : string * string -> isa_preference_table -> isa_preference_table

structure Preferences : PREFERENCES =

val thm_depsN = "thm_deps";    (* also in proof_general_pgip.ML: move to pgip_isabelle? *)

type pgiptype = PgipTypes.pgiptype

type isa_preference = { name: string,
                        descr: string,
                        default: string,
                        pgiptype: pgiptype,
                        get: unit -> string,
                        set: string -> unit }

fun mkpref get set typ nm descr =
    { name=nm, descr=descr, pgiptype=typ, get=get, set=set, default=get() } : isa_preference

fun mkpref_from_ref read write typ r nm descr =
    mkpref (fn()=> read (!r)) (fn v=> r:= (write v)) typ nm descr

val int_pref =
    mkpref_from_ref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE,NONE))
                    (PgipTypes.Pgipint (NONE, NONE))
val nat_pref =
    mkpref_from_ref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat

val bool_pref =
    mkpref_from_ref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool

val proof_pref =
        fun get () = PgipTypes.bool_to_pgstring (! proofs >= 2)
        fun set s = proofs := (if PgipTypes.read_pgipbool s then 2 else 1)
        mkpref get set PgipTypes.Pgipbool "full-proofs"
               "Record full proof objects internally"

val thm_deps_pref =
        fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN)
        fun set s =  NAMED_CRITICAL "print_mode" (fn () =>
          if PgipTypes.read_pgipbool s then
            change print_mode (insert (op =) thm_depsN)
            change print_mode (remove (op =) thm_depsN))
        mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
               "Track theorem dependencies within Proof General"

val print_depth_pref =
        fun get () = PgipTypes.int_to_pgstring (get_print_depth ())
        val set = print_depth o PgipTypes.read_pgipnat
        mkpref get set PgipTypes.Pgipnat
               "print-depth" "Setting for the ML print depth"

val display_preferences =
    [bool_pref show_types
               "Include types in display of Isabelle terms",
     bool_pref show_sorts
               "Include sorts in display of Isabelle terms",
     bool_pref show_consts
               "Show types of consts in Isabelle goal display",
     bool_pref long_names
               "Show fully qualified names in Isabelle terms",
     bool_pref show_brackets
               "Show full bracketing in Isabelle terms",
     bool_pref Proof.show_main_goal
               "Show main goal in proof state display",
     bool_pref Syntax.eta_contract
               "Print terms eta-contracted"]

val advanced_display_preferences =
    [nat_pref goals_limit
              "Setting for maximum number of goals printed",
     int_pref ProofContext.prems_limit
              "Setting for maximum number of premises printed",
     bool_pref show_question_marks
               "Show leading question mark of variable name"]

val tracing_preferences =
    [bool_pref trace_simp
               "Trace simplification rules.",
     nat_pref trace_simp_depth_limit
              "Trace simplifier depth limit.",
     bool_pref trace_rules
               "Trace application of the standard rules",
     bool_pref Pattern.trace_unify_fail
               "Output error diagnostics during unification",
     bool_pref Output.timing
               "Whether to enable timing in Isabelle.",
     bool_pref Toplevel.debug
                "Whether to enable debugging.",
     bool_pref Codegen.auto_quickcheck
                "Whether to enable quickcheck automatically.",
     nat_pref Codegen.auto_quickcheck_time_limit
                "Time limit for automatic quickcheck (in milliseconds)."]

val proof_preferences =
    [bool_pref quick_and_dirty
               "Take a few short cuts",
     bool_pref Toplevel.skip_proofs
               "Skip over proofs (interactive-only)",
     nat_pref Multithreading.max_threads
               "Maximum number of threads"]

val preferences =
    [("Display", display_preferences),
     ("Advanced Display", advanced_display_preferences),
     ("Tracing", tracing_preferences),
     ("Proof", proof_preferences)]

type isa_preference_table = (string * isa_preference list) list

fun remove name (preftable : isa_preference_table)  =
    map (fn (cat,prefs) =>
            (cat, filter_out (curry op= name o #name) prefs))

fun set_default (setname,newdefault) (preftable : isa_preference_table)  =
    map (fn (cat,prefs) =>
            (cat, map (fn (pref as {name,descr,default,pgiptype,get,set})
                          => if (name = setname) then
                                 (set newdefault;
                             else pref)