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