src/Pure/ProofGeneral/preferences.ML
author wenzelm
Mon May 13 13:23:13 2013 +0200 (2013-05-13)
changeset 51960 61ac1efe02c3
parent 51949 f6858bb224c9
child 51970 f08366cb9fd1
permissions -rw-r--r--
option "goals_limit", with more uniform description;
     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 options_pref: string -> string -> string -> preference
    21   val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
    22     'a Unsynchronized.ref -> string -> string -> preference
    23   val string_pref: string Unsynchronized.ref -> string -> string -> preference
    24   val real_pref: real Unsynchronized.ref -> string -> string -> preference
    25   val int_pref: int Unsynchronized.ref -> string -> string -> preference
    26   val nat_pref: int Unsynchronized.ref -> string -> string -> preference
    27   val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
    28   type T = (string * preference list) list
    29   val pure_preferences: T
    30   val remove: string -> T -> T
    31   val add: string -> preference -> T -> T
    32   val set_default: string * string -> T -> T
    33 end
    34 
    35 structure Preferences: PREFERENCES =
    36 struct
    37 
    38 (* categories *)
    39 
    40 val category_display = "Display";
    41 val category_advanced_display = "Advanced Display";
    42 val category_tracing = "Tracing";
    43 val category_proof = "Proof"
    44 
    45 
    46 (* preferences and preference tables *)
    47 
    48 type preference =
    49  {name: string,
    50   descr: string,
    51   default: string,
    52   pgiptype: PgipTypes.pgiptype,
    53   get: unit -> string,
    54   set: string -> unit};
    55 
    56 
    57 (* options as preferences *)
    58 
    59 fun options_pref option_name pgip_name descr : preference =
    60   let
    61     val typ = Options.default_typ option_name;
    62     val pgiptype =
    63       if typ = Options.boolT then PgipTypes.Pgipbool
    64       else if typ = Options.intT then PgipTypes.Pgipint (NONE, NONE)
    65       else if typ = Options.realT then PgipTypes.Pgipreal
    66       else PgipTypes.Pgipstring;
    67   in
    68    {name = pgip_name,
    69     descr = descr,
    70     default = Options.get_default option_name,
    71     pgiptype = pgiptype,
    72     get = fn () => Options.get_default option_name,
    73     set = Options.put_default option_name}
    74   end;
    75 
    76 
    77 (* generic preferences *)
    78 
    79 fun mkpref raw_get raw_set typ name descr : preference =
    80   let
    81     fun get () = CRITICAL raw_get;
    82     fun set x = CRITICAL (fn () => raw_set x);
    83   in {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()} end;
    84 
    85 fun generic_pref read write typ r =
    86   mkpref (fn () => read (! r)) (fn x => r := write x) typ;
    87 
    88 val string_pref = generic_pref I I PgipTypes.Pgipstring;
    89 
    90 val real_pref =
    91   generic_pref PgipTypes.real_to_pgstring PgipTypes.read_pgipreal PgipTypes.Pgipreal;
    92 
    93 val int_pref =
    94   generic_pref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE, NONE))
    95     (PgipTypes.Pgipint (NONE, NONE));
    96 
    97 val nat_pref =
    98   generic_pref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat;
    99 
   100 val bool_pref =
   101   generic_pref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool;
   102 
   103 
   104 (* preferences of Pure *)
   105 
   106 val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
   107   let
   108     fun get () = PgipTypes.bool_to_pgstring (Proofterm.proofs_enabled ());
   109     fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
   110   in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
   111 
   112 val parallel_proof_pref =
   113   let
   114     fun get () = PgipTypes.bool_to_pgstring (! Goal.parallel_proofs >= 1);
   115     fun set s = Goal.parallel_proofs := (if PgipTypes.read_pgipbool s then 1 else 0);
   116   in mkpref get set PgipTypes.Pgipbool "parallel-proofs" "Check proofs in parallel" end;
   117 
   118 val thm_depsN = "thm_deps";
   119 val thm_deps_pref =
   120   let
   121     fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN);
   122     fun set s =
   123       if PgipTypes.read_pgipbool s
   124       then Unsynchronized.change print_mode (insert (op =) thm_depsN)
   125       else Unsynchronized.change print_mode (remove (op =) thm_depsN);
   126   in
   127     mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
   128       "Track theorem dependencies within Proof General"
   129   end;
   130 
   131 val print_depth_pref =
   132   let
   133     fun get () = PgipTypes.int_to_pgstring (get_print_depth ());
   134     val set = print_depth o PgipTypes.read_pgipnat;
   135   in mkpref get set PgipTypes.Pgipnat "print-depth" "Setting for the ML print depth" end;
   136 
   137 
   138 val display_preferences =
   139  [bool_pref Printer.show_types_default
   140     "show-types"
   141     "Include types in display of Isabelle terms",
   142   bool_pref Printer.show_sorts_default
   143     "show-sorts"
   144     "Include sorts in display of Isabelle terms",
   145   bool_pref Goal_Display.show_consts_default
   146     "show-consts"
   147     "Show types of consts in Isabelle goal display",
   148   options_pref "names_long"
   149     "long-names"
   150     "Show fully qualified names in Isabelle terms",
   151   bool_pref Printer.show_brackets_default
   152     "show-brackets"
   153     "Show full bracketing in Isabelle terms",
   154   bool_pref Goal_Display.show_main_goal_default
   155     "show-main-goal"
   156     "Show main goal in proof state display",
   157   bool_pref Syntax_Trans.eta_contract_default
   158     "eta-contract"
   159     "Print terms eta-contracted"];
   160 
   161 val advanced_display_preferences =
   162  [options_pref "goals_limit"
   163     "goals-limit"
   164     "Setting for maximum number of subgoals to be printed",
   165   print_depth_pref,
   166   options_pref "show_question_marks"
   167     "show-question-marks"
   168     "Show leading question mark of variable name"];
   169 
   170 val tracing_preferences =
   171  [bool_pref Raw_Simplifier.simp_trace_default
   172     "trace-simplifier"
   173     "Trace simplification rules.",
   174   nat_pref Raw_Simplifier.simp_trace_depth_limit_default
   175     "trace-simplifier-depth"
   176     "Trace simplifier depth limit.",
   177   bool_pref Pattern.trace_unify_fail
   178     "trace-unification"
   179     "Output error diagnostics during unification",
   180   bool_pref Toplevel.timing
   181     "global-timing"
   182     "Whether to enable timing in Isabelle.",
   183   bool_pref Toplevel.debug
   184     "debugging"
   185     "Whether to enable debugging.",
   186   thm_deps_pref];
   187 
   188 val proof_preferences =
   189  [Unsynchronized.setmp quick_and_dirty true (fn () =>
   190     bool_pref quick_and_dirty
   191       "quick-and-dirty"
   192       "Take a few short cuts") (),
   193   bool_pref Goal.skip_proofs
   194     "skip-proofs"
   195     "Skip over proofs",
   196   proof_pref,
   197   nat_pref Multithreading.max_threads
   198     "max-threads"
   199     "Maximum number of threads",
   200   parallel_proof_pref];
   201 
   202 val pure_preferences =
   203  [(category_display, display_preferences),
   204   (category_advanced_display, advanced_display_preferences),
   205   (category_tracing, tracing_preferences),
   206   (category_proof, proof_preferences)];
   207 
   208 
   209 (* table of categories and preferences; names must be unique *)
   210 
   211 type T = (string * preference list) list;
   212 
   213 fun remove name (tab: T) = tab |> map
   214   (fn (cat, prefs) => (cat, filter_out (curry op = name o #name) prefs));
   215 
   216 fun set_default (setname, newdefault) (tab: T) = tab |> map
   217   (fn (cat, prefs) =>
   218     (cat, prefs |> map (fn (pref as {name, descr, default, pgiptype, get, set}) =>
   219       if name = setname then
   220         (set newdefault;
   221           {name =name , descr = descr, default = newdefault,
   222            pgiptype = pgiptype, get = get, set = set})
   223       else pref)));
   224 
   225 fun add cname (pref: preference) (tab: T) = tab |> map
   226   (fn (cat, prefs) =>
   227     if cat <> cname then (cat, prefs)
   228     else
   229       if exists (fn {name, ...} => name = #name pref) prefs
   230       then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs))
   231       else (cat, prefs @ [pref]));
   232 
   233 end;