src/Pure/ProofGeneral/preferences.ML
author wenzelm
Thu, 03 Feb 2011 19:21:12 +0100
changeset 41698 90597e044e5f
parent 41379 b31d7a1cd08f
child 42012 2c3fe3cbebae
permissions -rw-r--r--
clarified Proofterm.proofs_enabled;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     1
(*  Title:      Pure/ProofGeneral/preferences.ML
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     2
    Author:     David Aspinall and Markus Wenzel
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     3
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     4
User preferences for Isabelle which are maintained by the interface.
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     5
*)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     6
24329
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24191
diff changeset
     7
signature PREFERENCES =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     8
sig
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
     9
  val category_display: string
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
    10
  val category_advanced_display: string
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
    11
  val category_tracing: string
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
    12
  val category_proof: string
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    13
  type preference =
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    14
   {name: string,
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    15
    descr: string,
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    16
    default: string,
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    17
    pgiptype: PgipTypes.pgiptype,
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    18
    get: unit -> string,
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    19
    set: string -> unit}
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    20
  val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    21
    'a Unsynchronized.ref -> string -> string -> preference
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    22
  val string_pref: string Unsynchronized.ref -> string -> string -> preference
40292
ba13793594f0 support for real valued preferences;
wenzelm
parents: 39616
diff changeset
    23
  val real_pref: real Unsynchronized.ref -> string -> string -> preference
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    24
  val int_pref: int Unsynchronized.ref -> string -> string -> preference
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    25
  val nat_pref: int Unsynchronized.ref -> string -> string -> preference
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    26
  val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    27
  type T = (string * preference list) list
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    28
  val pure_preferences: T
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    29
  val remove: string -> T -> T
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    30
  val add: string -> preference -> T -> T
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    31
  val set_default: string * string -> T -> T
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    32
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    33
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    34
structure Preferences: PREFERENCES =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    35
struct
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    36
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
    37
(* categories *)
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
    38
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
    39
val category_display = "Display";
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
    40
val category_advanced_display = "Advanced Display";
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
    41
val category_tracing = "Tracing";
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
    42
val category_proof = "Proof"
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
    43
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
    44
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    45
(* preferences and preference tables *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    46
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    47
type preference =
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    48
 {name: string,
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    49
  descr: string,
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    50
  default: string,
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    51
  pgiptype: PgipTypes.pgiptype,
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    52
  get: unit -> string,
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    53
  set: string -> unit};
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    54
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    55
fun mkpref raw_get raw_set typ name descr : preference =
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    56
  let
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    57
    fun get () = CRITICAL raw_get;
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    58
    fun set x = CRITICAL (fn () => raw_set x);
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    59
  in {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()} end;
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    60
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    61
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    62
(* generic preferences *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    63
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    64
fun generic_pref read write typ r =
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    65
  mkpref (fn () => read (! r)) (fn x => r := write x) typ;
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    66
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    67
val string_pref = generic_pref I I PgipTypes.Pgipstring;
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    68
40292
ba13793594f0 support for real valued preferences;
wenzelm
parents: 39616
diff changeset
    69
val real_pref =
ba13793594f0 support for real valued preferences;
wenzelm
parents: 39616
diff changeset
    70
  generic_pref PgipTypes.real_to_pgstring PgipTypes.read_pgipreal PgipTypes.Pgipreal;
ba13793594f0 support for real valued preferences;
wenzelm
parents: 39616
diff changeset
    71
24329
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24191
diff changeset
    72
val int_pref =
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    73
  generic_pref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE, NONE))
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    74
    (PgipTypes.Pgipint (NONE, NONE));
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    75
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    76
val nat_pref =
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    77
  generic_pref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat;
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    78
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    79
val bool_pref =
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    80
  generic_pref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool;
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    81
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    82
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    83
(* preferences of Pure *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    84
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39165
diff changeset
    85
val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    86
  let
41698
90597e044e5f clarified Proofterm.proofs_enabled;
wenzelm
parents: 41379
diff changeset
    87
    fun get () = PgipTypes.bool_to_pgstring (Proofterm.proofs_enabled ());
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    88
    fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
    89
  in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    90
32061
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 30985
diff changeset
    91
val parallel_proof_pref =
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 30985
diff changeset
    92
  let
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 30985
diff changeset
    93
    fun get () = PgipTypes.bool_to_pgstring (! Goal.parallel_proofs >= 1);
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 30985
diff changeset
    94
    fun set s = Goal.parallel_proofs := (if PgipTypes.read_pgipbool s then 1 else 0);
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 30985
diff changeset
    95
  in mkpref get set PgipTypes.Pgipbool "parallel-proofs" "Check proofs in parallel" end;
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 30985
diff changeset
    96
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    97
val thm_depsN = "thm_deps";
24329
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24191
diff changeset
    98
val thm_deps_pref =
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
    99
  let
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   100
    fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN);
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   101
    fun set s =
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
   102
      if PgipTypes.read_pgipbool s
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
   103
      then Unsynchronized.change print_mode (insert (op =) thm_depsN)
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
   104
      else Unsynchronized.change print_mode (remove (op =) thm_depsN);
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   105
  in
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   106
    mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   107
      "Track theorem dependencies within Proof General"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   108
  end;
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   109
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   110
val print_depth_pref =
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   111
  let
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   112
    fun get () = PgipTypes.int_to_pgstring (get_print_depth ());
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   113
    val set = print_depth o PgipTypes.read_pgipnat;
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   114
  in mkpref get set PgipTypes.Pgipnat "print-depth" "Setting for the ML print depth" end;
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   115
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   116
24329
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24191
diff changeset
   117
val display_preferences =
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39128
diff changeset
   118
 [bool_pref show_types_default
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   119
    "show-types"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   120
    "Include types in display of Isabelle terms",
39134
917b4b6ba3d2 turned show_sorts/show_types into proper configuration options;
wenzelm
parents: 39128
diff changeset
   121
  bool_pref show_sorts_default
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   122
    "show-sorts"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   123
    "Include sorts in display of Isabelle terms",
39050
600de0485859 turned show_consts into proper configuration option;
wenzelm
parents: 38980
diff changeset
   124
  bool_pref show_consts_default
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   125
    "show-consts"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   126
    "Show types of consts in Isabelle goal display",
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   127
  bool_pref long_names
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   128
    "long-names"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   129
    "Show fully qualified names in Isabelle terms",
39137
ccb53edd59f0 turned show_brackets into proper configuration option;
wenzelm
parents: 39134
diff changeset
   130
  bool_pref show_brackets_default
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   131
    "show-brackets"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   132
    "Show full bracketing in Isabelle terms",
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39050
diff changeset
   133
  bool_pref Goal_Display.show_main_goal_default
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   134
    "show-main-goal"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   135
    "Show main goal in proof state display",
39128
93a7365fb4ee turned eta_contract into proper configuration option;
wenzelm
parents: 39125
diff changeset
   136
  bool_pref Syntax.eta_contract_default
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   137
    "eta-contract"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   138
    "Print terms eta-contracted"];
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   139
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   140
val advanced_display_preferences =
39125
f45d332a90e3 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents: 39050
diff changeset
   141
 [nat_pref Goal_Display.goals_limit_default
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   142
    "goals-limit"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   143
    "Setting for maximum number of goals printed",
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   144
  print_depth_pref,
38980
af73cf0dc31f turned show_question_marks into proper configuration option;
wenzelm
parents: 36006
diff changeset
   145
  bool_pref show_question_marks_default
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   146
    "show-question-marks"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   147
    "Show leading question mark of variable name"];
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   148
24329
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24191
diff changeset
   149
val tracing_preferences =
41228
e1fce873b814 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents: 41227
diff changeset
   150
 [bool_pref Raw_Simplifier.simp_trace_default
35995
26e820d27e0a re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
boehmes
parents: 35979
diff changeset
   151
    "trace-simplifier"
26e820d27e0a re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
boehmes
parents: 35979
diff changeset
   152
    "Trace simplification rules.",
41228
e1fce873b814 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents: 41227
diff changeset
   153
  nat_pref Raw_Simplifier.simp_trace_depth_limit_default
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   154
    "trace-simplifier-depth"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   155
    "Trace simplifier depth limit.",
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   156
  bool_pref Pattern.trace_unify_fail
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   157
    "trace-unification"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   158
    "Output error diagnostics during unification",
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   159
  bool_pref Output.timing
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   160
    "global-timing"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   161
    "Whether to enable timing in Isabelle.",
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   162
  bool_pref Toplevel.debug
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   163
    "debugging"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   164
    "Whether to enable debugging.",
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   165
  thm_deps_pref];
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   166
24329
f31594168d27 ML system provides get_print_depth;
wenzelm
parents: 24191
diff changeset
   167
val proof_preferences =
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39165
diff changeset
   168
 [Unsynchronized.setmp quick_and_dirty true (fn () =>
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
   169
    bool_pref quick_and_dirty
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
   170
      "quick-and-dirty"
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
   171
      "Take a few short cuts") (),
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   172
  bool_pref Toplevel.skip_proofs
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   173
    "skip-proofs"
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   174
    "Skip over proofs (interactive-only)",
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   175
  proof_pref,
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   176
  nat_pref Multithreading.max_threads
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   177
    "max-threads"
29435
a5f84ac14609 added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
wenzelm
parents: 28591
diff changeset
   178
    "Maximum number of threads",
32061
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 30985
diff changeset
   179
  parallel_proof_pref];
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   180
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   181
val pure_preferences =
30980
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
   182
 [(category_display, display_preferences),
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
   183
  (category_advanced_display, advanced_display_preferences),
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
   184
  (category_tracing, tracing_preferences),
fe0855471964 misc cleanup of auto_solve and quickcheck:
wenzelm
parents: 29858
diff changeset
   185
  (category_proof, proof_preferences)];
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   186
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   187
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   188
(* table of categories and preferences; names must be unique *)
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   189
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   190
type T = (string * preference list) list;
22214
6e9ab159512f Add operations on preference tables (remove, set_default).
aspinall
parents: 22130
diff changeset
   191
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   192
fun remove name (tab: T) = tab |> map
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   193
  (fn (cat, prefs) => (cat, filter_out (curry op = name o #name) prefs));
22214
6e9ab159512f Add operations on preference tables (remove, set_default).
aspinall
parents: 22130
diff changeset
   194
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   195
fun set_default (setname, newdefault) (tab: T) = tab |> map
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   196
  (fn (cat, prefs) =>
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   197
    (cat, prefs |> map (fn (pref as {name, descr, default, pgiptype, get, set}) =>
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   198
      if name = setname then
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   199
        (set newdefault;
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   200
          {name =name , descr = descr, default = newdefault,
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   201
           pgiptype = pgiptype, get = get, set = set})
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   202
      else pref)));
22214
6e9ab159512f Add operations on preference tables (remove, set_default).
aspinall
parents: 22130
diff changeset
   203
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   204
fun add cname (pref: preference) (tab: T) = tab |> map
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   205
  (fn (cat, prefs) =>
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   206
    if cat <> cname then (cat, prefs)
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   207
    else
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   208
      if exists (fn {name, ...} => name = #name pref) prefs
28591
790d1863be28 adding preferences is now permissive;
wenzelm
parents: 28587
diff changeset
   209
      then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs))
30985
2a22c6613dcf append prefs at end;
wenzelm
parents: 30980
diff changeset
   210
      else (cat, prefs @ [pref]));
28066
611e504c1191 extended interface to preferences to allow adding new ones
nipkow
parents: 25440
diff changeset
   211
28587
52ec4c827ed4 export generic_pref etc.;
wenzelm
parents: 28315
diff changeset
   212
end;