src/Pure/ProofGeneral/preferences.ML
author wenzelm
Tue Sep 29 11:49:22 2009 +0200 (2009-09-29)
changeset 32738 15bb09ca0378
parent 32061 11f8ee55662d
child 32966 5b21661fe618
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
     1 (*  Title:      Pure/ProofGeneral/preferences.ML
     2     Author:     David Aspinall and Markus Wenzel
     3 
     4 User preferences for Isabelle which are maintained by the interface.
     5 *)
     6 
     7 signature PREFERENCES =
     8 sig
     9   val category_display: string
    10   val category_advanced_display: string
    11   val category_tracing: string
    12   val category_proof: string
    13   type preference =
    14    {name: string,
    15     descr: string,
    16     default: string,
    17     pgiptype: PgipTypes.pgiptype,
    18     get: unit -> string,
    19     set: string -> unit}
    20   val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
    21     'a Unsynchronized.ref -> string -> string -> preference
    22   val string_pref: string Unsynchronized.ref -> string -> string -> preference
    23   val int_pref: int Unsynchronized.ref -> string -> string -> preference
    24   val nat_pref: int Unsynchronized.ref -> string -> string -> preference
    25   val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
    26   type T = (string * preference list) list
    27   val pure_preferences: T
    28   val remove: string -> T -> T
    29   val add: string -> preference -> T -> T
    30   val set_default: string * string -> T -> T
    31 end
    32 
    33 structure Preferences: PREFERENCES =
    34 struct
    35 
    36 (* categories *)
    37 
    38 val category_display = "Display";
    39 val category_advanced_display = "Advanced Display";
    40 val category_tracing = "Tracing";
    41 val category_proof = "Proof"
    42 
    43 
    44 (* preferences and preference tables *)
    45 
    46 type preference =
    47  {name: string,
    48   descr: string,
    49   default: string,
    50   pgiptype: PgipTypes.pgiptype,
    51   get: unit -> string,
    52   set: string -> unit};
    53 
    54 fun mkpref raw_get raw_set typ name descr : preference =
    55   let
    56     fun get () = CRITICAL raw_get;
    57     fun set x = CRITICAL (fn () => raw_set x);
    58   in {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()} end;
    59 
    60 
    61 (* generic preferences *)
    62 
    63 fun generic_pref read write typ r =
    64   mkpref (fn () => read (! r)) (fn x => r := write x) typ;
    65 
    66 val string_pref = generic_pref I I PgipTypes.Pgipstring;
    67 
    68 val int_pref =
    69   generic_pref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE, NONE))
    70     (PgipTypes.Pgipint (NONE, NONE));
    71 
    72 val nat_pref =
    73   generic_pref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat;
    74 
    75 val bool_pref =
    76   generic_pref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool;
    77 
    78 
    79 (* preferences of Pure *)
    80 
    81 val proof_pref = setmp Proofterm.proofs 1 (fn () =>
    82   let
    83     fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
    84     fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
    85   in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
    86 
    87 val parallel_proof_pref =
    88   let
    89     fun get () = PgipTypes.bool_to_pgstring (! Goal.parallel_proofs >= 1);
    90     fun set s = Goal.parallel_proofs := (if PgipTypes.read_pgipbool s then 1 else 0);
    91   in mkpref get set PgipTypes.Pgipbool "parallel-proofs" "Check proofs in parallel" end;
    92 
    93 val thm_depsN = "thm_deps";
    94 val thm_deps_pref =
    95   let
    96     fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN);
    97     fun set s =
    98       if PgipTypes.read_pgipbool s
    99       then Unsynchronized.change print_mode (insert (op =) thm_depsN)
   100       else Unsynchronized.change print_mode (remove (op =) thm_depsN);
   101   in
   102     mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
   103       "Track theorem dependencies within Proof General"
   104   end;
   105 
   106 val print_depth_pref =
   107   let
   108     fun get () = PgipTypes.int_to_pgstring (get_print_depth ());
   109     val set = print_depth o PgipTypes.read_pgipnat;
   110   in mkpref get set PgipTypes.Pgipnat "print-depth" "Setting for the ML print depth" end;
   111 
   112 
   113 val display_preferences =
   114  [bool_pref show_types
   115     "show-types"
   116     "Include types in display of Isabelle terms",
   117   bool_pref show_sorts
   118     "show-sorts"
   119     "Include sorts in display of Isabelle terms",
   120   bool_pref show_consts
   121     "show-consts"
   122     "Show types of consts in Isabelle goal display",
   123   bool_pref long_names
   124     "long-names"
   125     "Show fully qualified names in Isabelle terms",
   126   bool_pref show_brackets
   127     "show-brackets"
   128     "Show full bracketing in Isabelle terms",
   129   bool_pref Proof.show_main_goal
   130     "show-main-goal"
   131     "Show main goal in proof state display",
   132   bool_pref Syntax.eta_contract
   133     "eta-contract"
   134     "Print terms eta-contracted"];
   135 
   136 val advanced_display_preferences =
   137  [nat_pref goals_limit
   138     "goals-limit"
   139     "Setting for maximum number of goals printed",
   140   int_pref ProofContext.prems_limit
   141     "prems-limit"
   142     "Setting for maximum number of premises printed",
   143   print_depth_pref,
   144   bool_pref show_question_marks
   145     "show-question-marks"
   146     "Show leading question mark of variable name"];
   147 
   148 val tracing_preferences =
   149  [bool_pref trace_simp
   150     "trace-simplifier"
   151     "Trace simplification rules.",
   152   nat_pref trace_simp_depth_limit
   153     "trace-simplifier-depth"
   154     "Trace simplifier depth limit.",
   155   bool_pref trace_rules
   156     "trace-rules"
   157     "Trace application of the standard rules",
   158   bool_pref Pattern.trace_unify_fail
   159     "trace-unification"
   160     "Output error diagnostics during unification",
   161   bool_pref Output.timing
   162     "global-timing"
   163     "Whether to enable timing in Isabelle.",
   164   bool_pref Toplevel.debug
   165     "debugging"
   166     "Whether to enable debugging.",
   167   thm_deps_pref];
   168 
   169 val proof_preferences =
   170  [setmp quick_and_dirty true (fn () =>
   171     bool_pref quick_and_dirty
   172       "quick-and-dirty"
   173       "Take a few short cuts") (),
   174   bool_pref Toplevel.skip_proofs
   175     "skip-proofs"
   176     "Skip over proofs (interactive-only)",
   177   proof_pref,
   178   nat_pref Multithreading.max_threads
   179     "max-threads"
   180     "Maximum number of threads",
   181   parallel_proof_pref];
   182 
   183 val pure_preferences =
   184  [(category_display, display_preferences),
   185   (category_advanced_display, advanced_display_preferences),
   186   (category_tracing, tracing_preferences),
   187   (category_proof, proof_preferences)];
   188 
   189 
   190 (* table of categories and preferences; names must be unique *)
   191 
   192 type T = (string * preference list) list;
   193 
   194 fun remove name (tab: T) = tab |> map
   195   (fn (cat, prefs) => (cat, filter_out (curry op = name o #name) prefs));
   196 
   197 fun set_default (setname, newdefault) (tab: T) = tab |> map
   198   (fn (cat, prefs) =>
   199     (cat, prefs |> map (fn (pref as {name, descr, default, pgiptype, get, set}) =>
   200       if name = setname then
   201         (set newdefault;
   202           {name =name , descr = descr, default = newdefault,
   203            pgiptype = pgiptype, get = get, set = set})
   204       else pref)));
   205 
   206 fun add cname (pref: preference) (tab: T) = tab |> map
   207   (fn (cat, prefs) =>
   208     if cat <> cname then (cat, prefs)
   209     else
   210       if exists (fn {name, ...} => name = #name pref) prefs
   211       then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs))
   212       else (cat, prefs @ [pref]));
   213 
   214 end;