src/Pure/ProofGeneral/preferences.ML

turned show_brackets into proper configuration option;
Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;

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

User preferences for Isabelle which are maintained by the interface.
*)

signature PREFERENCES =
sig
  val category_display: string
  val category_advanced_display: string
  val category_tracing: string
  val category_proof: string
  type preference =
   {name: string,
    descr: string,
    default: string,
    pgiptype: PgipTypes.pgiptype,
    get: unit -> string,
    set: string -> unit}
  val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
    'a Unsynchronized.ref -> string -> string -> preference
  val string_pref: string Unsynchronized.ref -> string -> string -> preference
  val int_pref: int Unsynchronized.ref -> string -> string -> preference
  val nat_pref: int Unsynchronized.ref -> string -> string -> preference
  val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
  type T = (string * preference list) list
  val pure_preferences: T
  val remove: string -> T -> T
  val add: string -> preference -> T -> T
  val set_default: string * string -> T -> T
end

structure Preferences: PREFERENCES =
struct

(* categories *)

val category_display = "Display";
val category_advanced_display = "Advanced Display";
val category_tracing = "Tracing";
val category_proof = "Proof"


(* preferences and preference tables *)

type preference =
 {name: string,
  descr: string,
  default: string,
  pgiptype: PgipTypes.pgiptype,
  get: unit -> string,
  set: string -> unit};

fun mkpref raw_get raw_set typ name descr : preference =
  let
    fun get () = CRITICAL raw_get;
    fun set x = CRITICAL (fn () => raw_set x);
  in {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()} end;


(* generic preferences *)

fun generic_pref read write typ r =
  mkpref (fn () => read (! r)) (fn x => r := write x) typ;

val string_pref = generic_pref I I PgipTypes.Pgipstring;

val int_pref =
  generic_pref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE, NONE))
    (PgipTypes.Pgipint (NONE, NONE));

val nat_pref =
  generic_pref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat;

val bool_pref =
  generic_pref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool;


(* preferences of Pure *)

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

val parallel_proof_pref =
  let
    fun get () = PgipTypes.bool_to_pgstring (! Goal.parallel_proofs >= 1);
    fun set s = Goal.parallel_proofs := (if PgipTypes.read_pgipbool s then 1 else 0);
  in mkpref get set PgipTypes.Pgipbool "parallel-proofs" "Check proofs in parallel" end;

val thm_depsN = "thm_deps";
val thm_deps_pref =
  let
    fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN);
    fun set s =
      if PgipTypes.read_pgipbool s
      then Unsynchronized.change print_mode (insert (op =) thm_depsN)
      else Unsynchronized.change print_mode (remove (op =) thm_depsN);
  in
    mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
      "Track theorem dependencies within Proof General"
  end;

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


val display_preferences =
 [bool_pref show_types_default
    "show-types"
    "Include types in display of Isabelle terms",
  bool_pref show_sorts_default
    "show-sorts"
    "Include sorts in display of Isabelle terms",
  bool_pref show_consts_default
    "show-consts"
    "Show types of consts in Isabelle goal display",
  bool_pref long_names
    "long-names"
    "Show fully qualified names in Isabelle terms",
  bool_pref show_brackets_default
    "show-brackets"
    "Show full bracketing in Isabelle terms",
  bool_pref Goal_Display.show_main_goal_default
    "show-main-goal"
    "Show main goal in proof state display",
  bool_pref Syntax.eta_contract_default
    "eta-contract"
    "Print terms eta-contracted"];

val advanced_display_preferences =
 [nat_pref Goal_Display.goals_limit_default
    "goals-limit"
    "Setting for maximum number of goals printed",
  int_pref ProofContext.prems_limit
    "prems-limit"
    "Setting for maximum number of premises printed",
  print_depth_pref,
  bool_pref show_question_marks_default
    "show-question-marks"
    "Show leading question mark of variable name"];

val tracing_preferences =
 [bool_pref trace_simp_default
    "trace-simplifier"
    "Trace simplification rules.",
  nat_pref trace_simp_depth_limit
    "trace-simplifier-depth"
    "Trace simplifier depth limit.",
  bool_pref trace_rules
    "trace-rules"
    "Trace application of the standard rules",
  bool_pref Pattern.trace_unify_fail
    "trace-unification"
    "Output error diagnostics during unification",
  bool_pref Output.timing
    "global-timing"
    "Whether to enable timing in Isabelle.",
  bool_pref Toplevel.debug
    "debugging"
    "Whether to enable debugging.",
  thm_deps_pref];

val proof_preferences =
 [setmp_CRITICAL quick_and_dirty true (fn () =>
    bool_pref quick_and_dirty
      "quick-and-dirty"
      "Take a few short cuts") (),
  bool_pref Toplevel.skip_proofs
    "skip-proofs"
    "Skip over proofs (interactive-only)",
  proof_pref,
  nat_pref Multithreading.max_threads
    "max-threads"
    "Maximum number of threads",
  parallel_proof_pref];

val pure_preferences =
 [(category_display, display_preferences),
  (category_advanced_display, advanced_display_preferences),
  (category_tracing, tracing_preferences),
  (category_proof, proof_preferences)];


(* table of categories and preferences; names must be unique *)

type T = (string * preference list) list;

fun remove name (tab: T) = tab |> map
  (fn (cat, prefs) => (cat, filter_out (curry op = name o #name) prefs));

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

fun add cname (pref: preference) (tab: T) = tab |> map
  (fn (cat, prefs) =>
    if cat <> cname then (cat, prefs)
    else
      if exists (fn {name, ...} => name = #name pref) prefs
      then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs))
      else (cat, prefs @ [pref]));

end;