# HG changeset patch
# User wenzelm
# Date 1368649824 -7200
# Node ID bc0238c1f73a22f1ed0f6c9364428e18e663c250
# Parent  4b77f444afbb25b35cb8da5229e1a99b7a428983
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;

diff -r 4b77f444afbb -r bc0238c1f73a src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed May 15 22:02:51 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed May 15 22:30:24 2013 +0200
@@ -37,7 +37,10 @@
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
-    auto "auto-nitpick" "Run Nitpick automatically"
+    NONE
+    auto
+    "auto-nitpick"
+    "Run Nitpick automatically"
 
 type raw_param = string * string list
 
diff -r 4b77f444afbb -r bc0238c1f73a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed May 15 22:02:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed May 15 22:30:24 2013 +0200
@@ -46,7 +46,10 @@
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
-    auto "auto-sledgehammer" "Run Sledgehammer automatically"
+    NONE
+    auto
+    "auto-sledgehammer"
+    "Run Sledgehammer automatically"
 
 (** Sledgehammer commands **)
 
@@ -66,12 +69,14 @@
 
 val _ =
   ProofGeneral.preference_string ProofGeneral.category_proof
+    NONE
     provers
     "Sledgehammer: Provers"
     "Default automatic provers (separated by whitespace)"
 
 val _ =
   ProofGeneral.preference_int ProofGeneral.category_proof
+    NONE
     timeout
     "Sledgehammer: Time Limit"
     "ATPs will be interrupted after this time (in seconds)"
diff -r 4b77f444afbb -r bc0238c1f73a src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Wed May 15 22:02:51 2013 +0200
+++ b/src/HOL/Tools/try0.ML	Wed May 15 22:30:24 2013 +0200
@@ -28,7 +28,10 @@
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
-    auto "auto-try0" "Try standard proof methods"
+    NONE
+    auto
+    "auto-try0"
+    "Try standard proof methods"
 
 val default_timeout = seconds 5.0
 
diff -r 4b77f444afbb -r bc0238c1f73a src/Pure/Tools/proof_general.ML
--- a/src/Pure/Tools/proof_general.ML	Wed May 15 22:02:51 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML	Wed May 15 22:30:24 2013 +0200
@@ -18,13 +18,17 @@
   val pgipint: pgiptype
   val pgipfloat: pgiptype
   val pgipstring: pgiptype
-  val preference: category -> (unit -> string) -> (string -> unit) ->
-    string -> string -> string -> unit
-  val preference_bool: category -> bool Unsynchronized.ref -> string -> string -> unit
-  val preference_int: category -> int Unsynchronized.ref -> string -> string -> unit
-  val preference_real: category -> real Unsynchronized.ref -> string -> string -> unit
-  val preference_string: category -> string Unsynchronized.ref -> string -> string -> unit
-  val preference_option: category -> string -> string -> string -> unit
+  val preference: category -> string option ->
+    (unit -> string) -> (string -> unit) -> string -> string -> string -> unit
+  val preference_bool: category -> string option ->
+    bool Unsynchronized.ref -> string -> string -> unit
+  val preference_int: category -> string option ->
+    int Unsynchronized.ref -> string -> string -> unit
+  val preference_real: category -> string option ->
+    real Unsynchronized.ref -> string -> string -> unit
+  val preference_string: category -> string option ->
+    string Unsynchronized.ref -> string -> string -> unit
+  val preference_option: category -> string option -> string -> string -> string -> unit
   structure ThyLoad: sig val add_path: string -> unit end
   val thm_deps: bool Unsynchronized.ref
   val proof_generalN: string
@@ -52,8 +56,8 @@
 
 type preference =
  {category: string,
+  override: string option,
   descr: string,
-  default: string,
   pgiptype: pgiptype,
   get: unit -> string,
   set: string -> unit};
@@ -79,32 +83,36 @@
 
 fun all_preferences () =
   rev (Synchronized.value preferences)
-  |> map (fn (name, {category, descr, default, pgiptype, ...}) =>
-    (category, {name = name, descr = descr, default = default, pgiptype = pgiptype}))
+  |> map (fn (name, {category, descr, pgiptype, get, ...}) =>
+    (category, {name = name, descr = descr, default = get (), pgiptype = pgiptype}))
   |> AList.group (op =);
 
+fun init_preferences () =
+  Synchronized.value preferences
+  |> List.app (fn (_, {set, override = SOME value, ...}) => set value | _ => ());
+
 end;
 
 
 
 (* raw preferences *)
 
-fun preference category get set typ name descr =
+fun preference category override get set typ name descr =
   add_preference name
-    {category = category, descr = descr, pgiptype = typ, get = get, set = set, default = get ()};
+    {category = category, override = override, descr = descr, pgiptype = typ, get = get, set = set};
 
-fun preference_ref category read write typ r =
-  preference category (fn () => read (! r)) (fn x => r := write x) typ;
+fun preference_ref category override read write typ r =
+  preference category override (fn () => read (! r)) (fn x => r := write x) typ;
 
-fun preference_bool category = preference_ref category Markup.print_bool Markup.parse_bool pgipbool;
-fun preference_int category = preference_ref category Markup.print_int Markup.parse_int pgipint;
-fun preference_real category = preference_ref category Markup.print_real Markup.parse_real pgipfloat;
-fun preference_string category = preference_ref category I I pgipstring;
+fun preference_bool x y = preference_ref x y Markup.print_bool Markup.parse_bool pgipbool;
+fun preference_int x y = preference_ref x y Markup.print_int Markup.parse_int pgipint;
+fun preference_real x y = preference_ref x y Markup.print_real Markup.parse_real pgipfloat;
+fun preference_string x y = preference_ref x y I I pgipstring;
 
 
 (* system options *)
 
-fun preference_option category option_name pgip_name descr =
+fun preference_option category override option_name pgip_name descr =
   let
     val typ = Options.default_typ option_name;
     val pgiptype =
@@ -115,8 +123,8 @@
   in
     add_preference pgip_name
      {category = category,
+      override = override,
       descr = descr,
-      default = Options.get_default option_name,
       pgiptype = pgiptype,
       get = fn () => Options.get_default option_name,
       set = Options.put_default option_name}
@@ -399,6 +407,7 @@
      setup_thy_loader ();
      setup_present_hook ();
      initialized := true);
+   init_preferences ();
    sync_thy_loader ();
    Unsynchronized.change print_mode (update (op =) proof_generalN);
    Secure.PG_setup ();
diff -r 4b77f444afbb -r bc0238c1f73a src/Pure/Tools/proof_general_pure.ML
--- a/src/Pure/Tools/proof_general_pure.ML	Wed May 15 22:02:51 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Wed May 15 22:30:24 2013 +0200
@@ -9,42 +9,49 @@
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_display
+    NONE
     Printer.show_types_default
     "show-types"
     "Include types in display of Isabelle terms";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_display
+    NONE
     Printer.show_sorts_default
     "show-sorts"
     "Include sorts in display of Isabelle terms";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_display
+    NONE
     Goal_Display.show_consts_default
     "show-consts"
     "Show types of consts in Isabelle goal display";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
+    NONE
     @{option names_long}
     "long-names"
     "Show fully qualified names in Isabelle terms";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_display
+    NONE
     Printer.show_brackets_default
     "show-brackets"
     "Show full bracketing in Isabelle terms";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_display
+    NONE
     Goal_Display.show_main_goal_default
     "show-main-goal"
     "Show main goal in proof state display";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_display
+    NONE
     Syntax_Trans.eta_contract_default
     "eta-contract"
     "Print terms eta-contracted";
@@ -54,12 +61,14 @@
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_advanced_display
+    NONE
     @{option goals_limit}
     "goals-limit"
     "Setting for maximum number of subgoals to be printed";
 
 val _ =
   ProofGeneral.preference ProofGeneral.category_advanced_display
+    NONE
     (Markup.print_int o get_print_depth)
     (print_depth o Markup.parse_int)
     ProofGeneral.pgipint
@@ -68,6 +77,7 @@
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_advanced_display
+    NONE
     @{option show_question_marks}
     "show-question-marks"
     "Show leading question mark of variable name";
@@ -77,36 +87,42 @@
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
+    NONE
     Raw_Simplifier.simp_trace_default
     "trace-simplifier"
     "Trace simplification rules";
 
 val _ =
   ProofGeneral.preference_int ProofGeneral.category_tracing
+    NONE
     Raw_Simplifier.simp_trace_depth_limit_default
     "trace-simplifier-depth"
     "Trace simplifier depth limit";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
+    NONE
     Pattern.trace_unify_fail
     "trace-unification"
     "Output error diagnostics during unification";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
+    NONE
     Toplevel.timing
     "global-timing"
     "Whether to enable timing in Isabelle";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
+    NONE
     Toplevel.debug
     "debugging"
     "Whether to enable debugging";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
+    NONE
     ProofGeneral.thm_deps
     "theorem-dependencies"
     "Track theorem dependencies within Proof General";
@@ -115,36 +131,38 @@
 (* proof *)
 
 val _ =
-  Unsynchronized.setmp quick_and_dirty true (fn () =>
-    ProofGeneral.preference_bool ProofGeneral.category_proof
-      quick_and_dirty
-      "quick-and-dirty"
-      "Take a few short cuts") ();
+  ProofGeneral.preference_bool ProofGeneral.category_proof
+    (SOME "true")
+    quick_and_dirty
+    "quick-and-dirty"
+    "Take a few short cuts";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_proof
+    NONE
     Goal.skip_proofs
     "skip-proofs"
     "Skip over proofs";
 
 val _ =
-  Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
-    ProofGeneral.preference ProofGeneral.category_proof
-      (Markup.print_bool o Proofterm.proofs_enabled)
-      (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1))
-      ProofGeneral.pgipbool
-      "full-proofs"
-      "Record full proof objects internally") ();
+  ProofGeneral.preference ProofGeneral.category_proof
+    NONE
+    (Markup.print_bool o Proofterm.proofs_enabled)
+    (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1))
+    ProofGeneral.pgipbool
+    "full-proofs"
+    "Record full proof objects internally";
 
 val _ =
-  Unsynchronized.setmp Multithreading.max_threads 0 (fn () =>
-    ProofGeneral.preference_int ProofGeneral.category_proof
-      Multithreading.max_threads
-      "max-threads"
-      "Maximum number of threads") ();
+  ProofGeneral.preference_int ProofGeneral.category_proof
+    NONE
+    Multithreading.max_threads
+    "max-threads"
+    "Maximum number of threads";
 
 val _ =
   ProofGeneral.preference ProofGeneral.category_proof
+    NONE
     (fn () => Markup.print_bool (! Goal.parallel_proofs >= 1))
     (fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0))
     ProofGeneral.pgipbool
diff -r 4b77f444afbb -r bc0238c1f73a src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed May 15 22:02:51 2013 +0200
+++ b/src/Tools/quickcheck.ML	Wed May 15 22:30:24 2013 +0200
@@ -97,11 +97,11 @@
 val auto = Unsynchronized.ref false;
 
 val _ =
-  Unsynchronized.setmp auto true (fn () =>
-    ProofGeneral.preference_bool ProofGeneral.category_tracing
-      auto
-      "auto-quickcheck"
-      "Run Quickcheck automatically") ()
+  ProofGeneral.preference_bool ProofGeneral.category_tracing
+    (SOME "true")
+    auto
+    "auto-quickcheck"
+    "Run Quickcheck automatically";
 
 
 (* quickcheck report *)
diff -r 4b77f444afbb -r bc0238c1f73a src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Wed May 15 22:02:51 2013 +0200
+++ b/src/Tools/solve_direct.ML	Wed May 15 22:30:24 2013 +0200
@@ -37,11 +37,11 @@
 val max_solutions = Unsynchronized.ref 5;
 
 val _ =
-  Unsynchronized.setmp auto true (fn () =>
-    ProofGeneral.preference_bool ProofGeneral.category_tracing
-      auto
-      "auto-solve-direct"
-      ("Run " ^ quote solve_directN ^ " automatically")) ();
+  ProofGeneral.preference_bool ProofGeneral.category_tracing
+    (SOME "true")
+    auto
+    "auto-solve-direct"
+    ("Run " ^ quote solve_directN ^ " automatically");
 
 
 (* solve_direct command *)
diff -r 4b77f444afbb -r bc0238c1f73a src/Tools/try.ML
--- a/src/Tools/try.ML	Wed May 15 22:02:51 2013 +0200
+++ b/src/Tools/try.ML	Wed May 15 22:30:24 2013 +0200
@@ -36,6 +36,7 @@
 
 val _ =
   ProofGeneral.preference_real ProofGeneral.category_tracing
+    NONE
     auto_time_limit
     "auto-try-time-limit"
     "Time limit for automatically tried tools (in seconds)"