renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
authorwenzelm
Wed Sep 22 18:21:48 2010 +0200 (2010-09-22)
changeset 396168052101883c3
parent 39615 b926f8ec9cac
child 39617 a58eba339d2b
child 39642 dd7b582f6929
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
NEWS
src/HOL/Import/HOL/ROOT.ML
src/HOL/Induct/ROOT.ML
src/HOL/Nitpick_Examples/ROOT.ML
src/HOL/Nominal/Examples/ROOT.ML
src/HOL/Predicate_Compile_Examples/ROOT.ML
src/HOL/Tools/try.ML
src/Pure/Isar/proof.ML
src/Pure/ML-Systems/multithreading.ML
src/Pure/ML-Systems/multithreading_polyml.ML
src/Pure/ML-Systems/polyml-5.2.1.ML
src/Pure/ML-Systems/polyml-5.2.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML-Systems/thread_dummy.ML
src/Pure/ML-Systems/unsynchronized.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/System/session.ML
src/Pure/Thy/html.ML
src/Pure/Thy/present.ML
src/Pure/library.ML
src/Tools/auto_solve.ML
src/Tools/quickcheck.ML
     1.1 --- a/NEWS	Wed Sep 22 17:46:59 2010 +0200
     1.2 +++ b/NEWS	Wed Sep 22 18:21:48 2010 +0200
     1.3 @@ -244,6 +244,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
     1.8 +meaning.
     1.9 +
    1.10  * Renamed structure PureThy to Pure_Thy and moved most of its
    1.11  operations to structure Global_Theory, to emphasize that this is
    1.12  rarely-used global-only stuff.
     2.1 --- a/src/HOL/Import/HOL/ROOT.ML	Wed Sep 22 17:46:59 2010 +0200
     2.2 +++ b/src/HOL/Import/HOL/ROOT.ML	Wed Sep 22 18:21:48 2010 +0200
     2.3 @@ -1,2 +1,2 @@
     2.4  use_thy "~~/src/HOL/Old_Number_Theory/Primes";
     2.5 -setmp_noncritical quick_and_dirty true use_thys ["HOL4Prob", "HOL4"];
     2.6 +Unsynchronized.setmp quick_and_dirty true use_thys ["HOL4Prob", "HOL4"];
     3.1 --- a/src/HOL/Induct/ROOT.ML	Wed Sep 22 17:46:59 2010 +0200
     3.2 +++ b/src/HOL/Induct/ROOT.ML	Wed Sep 22 18:21:48 2010 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -setmp_noncritical quick_and_dirty true
     3.5 +Unsynchronized.setmp quick_and_dirty true
     3.6    use_thys ["Common_Patterns"];
     3.7  
     3.8  use_thys ["QuoDataType", "QuoNestedDataType", "Term", "SList",
     4.1 --- a/src/HOL/Nitpick_Examples/ROOT.ML	Wed Sep 22 17:46:59 2010 +0200
     4.2 +++ b/src/HOL/Nitpick_Examples/ROOT.ML	Wed Sep 22 18:21:48 2010 +0200
     4.3 @@ -5,4 +5,4 @@
     4.4  Nitpick examples.
     4.5  *)
     4.6  
     4.7 -setmp_noncritical quick_and_dirty true use_thys ["Nitpick_Examples"];
     4.8 +Unsynchronized.setmp quick_and_dirty true use_thys ["Nitpick_Examples"];
     5.1 --- a/src/HOL/Nominal/Examples/ROOT.ML	Wed Sep 22 17:46:59 2010 +0200
     5.2 +++ b/src/HOL/Nominal/Examples/ROOT.ML	Wed Sep 22 18:21:48 2010 +0200
     5.3 @@ -1,3 +1,3 @@
     5.4  use_thys ["Nominal_Examples"];
     5.5  
     5.6 -setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"]; 
     5.7 +Unsynchronized.setmp quick_and_dirty true use_thys ["VC_Condition"];
     6.1 --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Wed Sep 22 17:46:59 2010 +0200
     6.2 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Wed Sep 22 18:21:48 2010 +0200
     6.3 @@ -1,5 +1,20 @@
     6.4 -use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples", "IMP_1", "IMP_2", "IMP_3", "IMP_4"];
     6.5 +use_thys [
     6.6 +  "Predicate_Compile_Examples",
     6.7 +  "Predicate_Compile_Quickcheck_Examples",
     6.8 +  "Specialisation_Examples",
     6.9 +  "IMP_1",
    6.10 +  "IMP_2",
    6.11 +  "IMP_3",
    6.12 +  "IMP_4"];
    6.13 +
    6.14  if getenv "EXEC_SWIPL" = "" andalso getenv "EXEC_YAP" = "" then
    6.15 -  (warning "No prolog system found - could not use example theories that require a prolog system"; ())
    6.16 +  (warning "No prolog system found - skipping some example theories"; ())
    6.17  else
    6.18 -  (use_thys ["Code_Prolog_Examples", "Context_Free_Grammar_Example", "Hotel_Example", "Lambda_Example", "List_Examples"]; setmp_noncritical quick_and_dirty true use_thys ["Reg_Exp_Example"])
    6.19 +  (use_thys [
    6.20 +    "Code_Prolog_Examples",
    6.21 +    "Context_Free_Grammar_Example",
    6.22 +    "Hotel_Example",
    6.23 +    "Lambda_Example",
    6.24 +    "List_Examples"];
    6.25 +   Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"]);
    6.26 +
     7.1 --- a/src/HOL/Tools/try.ML	Wed Sep 22 17:46:59 2010 +0200
     7.2 +++ b/src/HOL/Tools/try.ML	Wed Sep 22 18:21:48 2010 +0200
     7.3 @@ -18,7 +18,7 @@
     7.4  
     7.5  val _ =
     7.6    ProofGeneralPgip.add_preference Preferences.category_tracing
     7.7 -  (setmp_noncritical auto true (fn () =>
     7.8 +  (Unsynchronized.setmp auto true (fn () =>
     7.9      Preferences.bool_pref auto
    7.10        "auto-try" "Try standard proof methods.") ());
    7.11  
     8.1 --- a/src/Pure/Isar/proof.ML	Wed Sep 22 17:46:59 2010 +0200
     8.2 +++ b/src/Pure/Isar/proof.ML	Wed Sep 22 18:21:48 2010 +0200
     8.3 @@ -976,7 +976,7 @@
     8.4        else ();
     8.5      val test_proof =
     8.6        try (local_skip_proof true)
     8.7 -      |> setmp_noncritical testing true
     8.8 +      |> Unsynchronized.setmp testing true
     8.9        |> Exn.capture;
    8.10  
    8.11      fun after_qed' results =
     9.1 --- a/src/Pure/ML-Systems/multithreading.ML	Wed Sep 22 17:46:59 2010 +0200
     9.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Wed Sep 22 18:21:48 2010 +0200
     9.3 @@ -14,7 +14,7 @@
     9.4  sig
     9.5    include BASIC_MULTITHREADING
     9.6    val available: bool
     9.7 -  val max_threads: int Unsynchronized.ref
     9.8 +  val max_threads: int ref
     9.9    val max_threads_value: unit -> int
    9.10    val enabled: unit -> bool
    9.11    val no_interrupts: Thread.threadAttribute list
    9.12 @@ -24,7 +24,7 @@
    9.13    val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
    9.14    val sync_wait: Thread.threadAttribute list option -> Time.time option ->
    9.15      ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
    9.16 -  val trace: int Unsynchronized.ref
    9.17 +  val trace: int ref
    9.18    val tracing: int -> (unit -> string) -> unit
    9.19    val tracing_time: bool -> Time.time -> (unit -> string) -> unit
    9.20    val real_time: ('a -> unit) -> 'a -> Time.time
    9.21 @@ -38,7 +38,7 @@
    9.22  (* options *)
    9.23  
    9.24  val available = false;
    9.25 -val max_threads = Unsynchronized.ref (1: int);
    9.26 +val max_threads = ref (1: int);
    9.27  fun max_threads_value () = 1: int;
    9.28  fun enabled () = false;
    9.29  
    9.30 @@ -57,7 +57,7 @@
    9.31  
    9.32  (* tracing *)
    9.33  
    9.34 -val trace = Unsynchronized.ref (0: int);
    9.35 +val trace = ref (0: int);
    9.36  fun tracing _ _ = ();
    9.37  fun tracing_time _ _ _ = ();
    9.38  fun real_time f x = (f x; Time.zeroTime);
    9.39 @@ -72,7 +72,7 @@
    9.40  
    9.41  (* serial numbers *)
    9.42  
    9.43 -local val count = Unsynchronized.ref (0: int)
    9.44 +local val count = ref (0: int)
    9.45  in fun serial () = (count := ! count + 1; ! count) end;
    9.46  
    9.47  end;
    10.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Sep 22 17:46:59 2010 +0200
    10.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Sep 22 18:21:48 2010 +0200
    10.3 @@ -31,7 +31,7 @@
    10.4  
    10.5  val available = true;
    10.6  
    10.7 -val max_threads = Unsynchronized.ref 0;
    10.8 +val max_threads = ref 0;
    10.9  
   10.10  fun max_threads_value () =
   10.11    let val m = ! max_threads in
   10.12 @@ -109,7 +109,7 @@
   10.13  
   10.14  (* tracing *)
   10.15  
   10.16 -val trace = Unsynchronized.ref 0;
   10.17 +val trace = ref 0;
   10.18  
   10.19  fun tracing level msg =
   10.20    if level > ! trace then ()
   10.21 @@ -143,7 +143,7 @@
   10.22  fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
   10.23    let
   10.24      val worker = Thread.self ();
   10.25 -    val timeout = Unsynchronized.ref false;
   10.26 +    val timeout = ref false;
   10.27      val watchdog = Thread.fork (fn () =>
   10.28        (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
   10.29  
   10.30 @@ -168,7 +168,7 @@
   10.31  
   10.32      (*result state*)
   10.33      datatype result = Wait | Signal | Result of int;
   10.34 -    val result = Unsynchronized.ref Wait;
   10.35 +    val result = ref Wait;
   10.36      val lock = Mutex.mutex ();
   10.37      val cond = ConditionVar.conditionVar ();
   10.38      fun set_result res =
   10.39 @@ -226,8 +226,8 @@
   10.40  local
   10.41  
   10.42  val critical_lock = Mutex.mutex ();
   10.43 -val critical_thread = Unsynchronized.ref (NONE: Thread.thread option);
   10.44 -val critical_name = Unsynchronized.ref "";
   10.45 +val critical_thread = ref (NONE: Thread.thread option);
   10.46 +val critical_name = ref "";
   10.47  
   10.48  in
   10.49  
   10.50 @@ -269,7 +269,7 @@
   10.51  local
   10.52  
   10.53  val serial_lock = Mutex.mutex ();
   10.54 -val serial_count = Unsynchronized.ref 0;
   10.55 +val serial_count = ref 0;
   10.56  
   10.57  in
   10.58  
    11.1 --- a/src/Pure/ML-Systems/polyml-5.2.1.ML	Wed Sep 22 17:46:59 2010 +0200
    11.2 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML	Wed Sep 22 18:21:48 2010 +0200
    11.3 @@ -3,8 +3,6 @@
    11.4  Compatibility wrapper for Poly/ML 5.2.1.
    11.5  *)
    11.6  
    11.7 -use "ML-Systems/unsynchronized.ML";
    11.8 -
    11.9  open Thread;
   11.10  
   11.11  structure ML_Name_Space =
   11.12 @@ -18,6 +16,10 @@
   11.13  
   11.14  use "ML-Systems/polyml_common.ML";
   11.15  use "ML-Systems/multithreading_polyml.ML";
   11.16 +use "ML-Systems/unsynchronized.ML";
   11.17 +
   11.18 +val _ = PolyML.Compiler.forgetValue "ref";
   11.19 +val _ = PolyML.Compiler.forgetType "ref";
   11.20  
   11.21  val pointer_eq = PolyML.pointerEq;
   11.22  
    12.1 --- a/src/Pure/ML-Systems/polyml-5.2.ML	Wed Sep 22 17:46:59 2010 +0200
    12.2 +++ b/src/Pure/ML-Systems/polyml-5.2.ML	Wed Sep 22 18:21:48 2010 +0200
    12.3 @@ -3,8 +3,6 @@
    12.4  Compatibility wrapper for Poly/ML 5.2.
    12.5  *)
    12.6  
    12.7 -use "ML-Systems/unsynchronized.ML";
    12.8 -
    12.9  open Thread;
   12.10  
   12.11  structure ML_Name_Space =
   12.12 @@ -17,9 +15,12 @@
   12.13  fun reraise exn = raise exn;
   12.14  
   12.15  use "ML-Systems/polyml_common.ML";
   12.16 -
   12.17  use "ML-Systems/thread_dummy.ML";
   12.18  use "ML-Systems/multithreading.ML";
   12.19 +use "ML-Systems/unsynchronized.ML";
   12.20 +
   12.21 +val _ = PolyML.Compiler.forgetValue "ref";
   12.22 +val _ = PolyML.Compiler.forgetType "ref";
   12.23  
   12.24  val pointer_eq = PolyML.pointerEq;
   12.25  
    13.1 --- a/src/Pure/ML-Systems/polyml.ML	Wed Sep 22 17:46:59 2010 +0200
    13.2 +++ b/src/Pure/ML-Systems/polyml.ML	Wed Sep 22 18:21:48 2010 +0200
    13.3 @@ -3,8 +3,6 @@
    13.4  Compatibility wrapper for Poly/ML 5.3 and 5.4.
    13.5  *)
    13.6  
    13.7 -use "ML-Systems/unsynchronized.ML";
    13.8 -
    13.9  open Thread;
   13.10  
   13.11  structure ML_Name_Space =
   13.12 @@ -21,6 +19,10 @@
   13.13  
   13.14  use "ML-Systems/polyml_common.ML";
   13.15  use "ML-Systems/multithreading_polyml.ML";
   13.16 +use "ML-Systems/unsynchronized.ML";
   13.17 +
   13.18 +val _ = PolyML.Compiler.forgetValue "ref";
   13.19 +val _ = PolyML.Compiler.forgetType "ref";
   13.20  
   13.21  val pointer_eq = PolyML.pointerEq;
   13.22  
    14.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Wed Sep 22 17:46:59 2010 +0200
    14.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Wed Sep 22 18:21:48 2010 +0200
    14.3 @@ -29,8 +29,6 @@
    14.4  val _ = PolyML.Compiler.forgetValue "foldl";
    14.5  val _ = PolyML.Compiler.forgetValue "foldr";
    14.6  val _ = PolyML.Compiler.forgetValue "print";
    14.7 -val _ = PolyML.Compiler.forgetValue "ref";
    14.8 -val _ = PolyML.Compiler.forgetType "ref";
    14.9  
   14.10  
   14.11  (* Compiler options *)
   14.12 @@ -62,7 +60,7 @@
   14.13  (* toplevel printing *)
   14.14  
   14.15  local
   14.16 -  val depth = Unsynchronized.ref 10;
   14.17 +  val depth = ref 10;
   14.18  in
   14.19    fun get_print_depth () = ! depth;
   14.20    fun print_depth n = (depth := n; PolyML.print_depth n);
    15.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Sep 22 17:46:59 2010 +0200
    15.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Sep 22 18:21:48 2010 +0200
    15.3 @@ -7,7 +7,6 @@
    15.4  fun reraise exn = raise exn;
    15.5  
    15.6  use "ML-Systems/proper_int.ML";
    15.7 -use "ML-Systems/unsynchronized.ML";
    15.8  use "ML-Systems/overloading_smlnj.ML";
    15.9  use "General/exn.ML";
   15.10  use "ML-Systems/single_assignment.ML";
   15.11 @@ -159,6 +158,9 @@
   15.12  end;
   15.13  
   15.14  
   15.15 +use "ML-Systems/unsynchronized.ML";
   15.16 +
   15.17 +
   15.18  
   15.19  (** OS related **)
   15.20  
    16.1 --- a/src/Pure/ML-Systems/thread_dummy.ML	Wed Sep 22 17:46:59 2010 +0200
    16.2 +++ b/src/Pure/ML-Systems/thread_dummy.ML	Wed Sep 22 18:21:48 2010 +0200
    16.3 @@ -60,7 +60,7 @@
    16.4  
    16.5  local
    16.6  
    16.7 -val data = Unsynchronized.ref ([]: Universal.universal  Unsynchronized.ref list);
    16.8 +val data = ref ([]: Universal.universal  ref list);
    16.9  
   16.10  fun find_data tag =
   16.11    let
   16.12 @@ -75,7 +75,7 @@
   16.13  fun setLocal (tag, x) =
   16.14    (case find_data tag of
   16.15      SOME r => r := Universal.tagInject tag x
   16.16 -  | NONE => data :=  Unsynchronized.ref (Universal.tagInject tag x) :: ! data);
   16.17 +  | NONE => data :=  ref (Universal.tagInject tag x) :: ! data);
   16.18  
   16.19  end;
   16.20  end;
    17.1 --- a/src/Pure/ML-Systems/unsynchronized.ML	Wed Sep 22 17:46:59 2010 +0200
    17.2 +++ b/src/Pure/ML-Systems/unsynchronized.ML	Wed Sep 22 18:21:48 2010 +0200
    17.3 @@ -18,4 +18,13 @@
    17.4  fun inc i = (i := ! i + (1: int); ! i);
    17.5  fun dec i = (i := ! i - (1: int); ! i);
    17.6  
    17.7 +fun setmp flag value f x =
    17.8 +  uninterruptible (fn restore_attributes => fn () =>
    17.9 +    let
   17.10 +      val orig_value = ! flag;
   17.11 +      val _ = flag := value;
   17.12 +      val result = Exn.capture (restore_attributes f) x;
   17.13 +      val _ = flag := orig_value;
   17.14 +    in Exn.release result end) ();
   17.15 +
   17.16  end;
    18.1 --- a/src/Pure/ProofGeneral/preferences.ML	Wed Sep 22 17:46:59 2010 +0200
    18.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Wed Sep 22 18:21:48 2010 +0200
    18.3 @@ -78,7 +78,7 @@
    18.4  
    18.5  (* preferences of Pure *)
    18.6  
    18.7 -val proof_pref = setmp_noncritical Proofterm.proofs 1 (fn () =>
    18.8 +val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
    18.9    let
   18.10      fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
   18.11      fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
   18.12 @@ -164,7 +164,7 @@
   18.13    thm_deps_pref];
   18.14  
   18.15  val proof_preferences =
   18.16 - [setmp_noncritical quick_and_dirty true (fn () =>
   18.17 + [Unsynchronized.setmp quick_and_dirty true (fn () =>
   18.18      bool_pref quick_and_dirty
   18.19        "quick-and-dirty"
   18.20        "Take a few short cuts") (),
    19.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Sep 22 17:46:59 2010 +0200
    19.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Sep 22 18:21:48 2010 +0200
    19.3 @@ -1044,7 +1044,7 @@
    19.4     This works for preferences but not generally guaranteed
    19.5     because we haven't done full setup here (e.g., no pgml mode)  *)
    19.6  fun process_pgip_emacs str =
    19.7 -     setmp_noncritical output_xml_fn (!pgip_output_channel) process_pgip_plain str
    19.8 +     Unsynchronized.setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str
    19.9  
   19.10  end
   19.11  
    20.1 --- a/src/Pure/System/session.ML	Wed Sep 22 17:46:59 2010 +0200
    20.2 +++ b/src/Pure/System/session.ML	Wed Sep 22 18:21:48 2010 +0200
    20.3 @@ -110,11 +110,11 @@
    20.4          in () end
    20.5        else use root;
    20.6        finish ()))
    20.7 -    |> setmp_noncritical Proofterm.proofs level
    20.8 -    |> setmp_noncritical print_mode (modes @ print_mode_value ())
    20.9 -    |> setmp_noncritical Goal.parallel_proofs parallel_proofs
   20.10 -    |> setmp_noncritical Multithreading.trace trace_threads
   20.11 -    |> setmp_noncritical Multithreading.max_threads
   20.12 +    |> Unsynchronized.setmp Proofterm.proofs level
   20.13 +    |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
   20.14 +    |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
   20.15 +    |> Unsynchronized.setmp Multithreading.trace trace_threads
   20.16 +    |> Unsynchronized.setmp Multithreading.max_threads
   20.17        (if Multithreading.available then max_threads
   20.18         else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
   20.19    handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
    21.1 --- a/src/Pure/Thy/html.ML	Wed Sep 22 17:46:59 2010 +0200
    21.2 +++ b/src/Pure/Thy/html.ML	Wed Sep 22 18:21:48 2010 +0200
    21.3 @@ -277,7 +277,7 @@
    21.4  (* document *)
    21.5  
    21.6  val charset = Unsynchronized.ref "ISO-8859-1";
    21.7 -fun with_charset s = setmp_noncritical charset s;   (* FIXME unreliable *)
    21.8 +fun with_charset s = Unsynchronized.setmp charset s;   (* FIXME unreliable *)
    21.9  
   21.10  fun begin_document title =
   21.11    let val cs = ! charset in
    22.1 --- a/src/Pure/Thy/present.ML	Wed Sep 22 17:46:59 2010 +0200
    22.2 +++ b/src/Pure/Thy/present.ML	Wed Sep 22 18:21:48 2010 +0200
    22.3 @@ -165,7 +165,7 @@
    22.4    CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
    22.5  
    22.6  val suppress_tex_source = Unsynchronized.ref false;
    22.7 -fun no_document f x = setmp_noncritical suppress_tex_source true f x;
    22.8 +fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;  (* FIXME unreliable *)
    22.9  
   22.10  fun init_theory_info name info =
   22.11    change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
    23.1 --- a/src/Pure/library.ML	Wed Sep 22 17:46:59 2010 +0200
    23.2 +++ b/src/Pure/library.ML	Wed Sep 22 18:21:48 2010 +0200
    23.3 @@ -56,7 +56,6 @@
    23.4    val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
    23.5    val exists: ('a -> bool) -> 'a list -> bool
    23.6    val forall: ('a -> bool) -> 'a list -> bool
    23.7 -  val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    23.8    val setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    23.9    val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
   23.10  
   23.11 @@ -306,18 +305,8 @@
   23.12  
   23.13  (* flags *)
   23.14  
   23.15 -(*temporarily set flag during execution*)
   23.16 -fun setmp_noncritical flag value f x =
   23.17 -  uninterruptible (fn restore_attributes => fn () =>
   23.18 -    let
   23.19 -      val orig_value = ! flag;
   23.20 -      val _ = flag := value;
   23.21 -      val result = Exn.capture (restore_attributes f) x;
   23.22 -      val _ = flag := orig_value;
   23.23 -    in Exn.release result end) ();
   23.24 -
   23.25  fun setmp_CRITICAL flag value f x =
   23.26 -  NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x);
   23.27 +  NAMED_CRITICAL "setmp" (fn () => Unsynchronized.setmp flag value f x);
   23.28  
   23.29  fun setmp_thread_data tag orig_data data f x =
   23.30    uninterruptible (fn restore_attributes => fn () =>
    24.1 --- a/src/Tools/auto_solve.ML	Wed Sep 22 17:46:59 2010 +0200
    24.2 +++ b/src/Tools/auto_solve.ML	Wed Sep 22 18:21:48 2010 +0200
    24.3 @@ -25,7 +25,7 @@
    24.4  
    24.5  val _ =
    24.6    ProofGeneralPgip.add_preference Preferences.category_tracing
    24.7 -  (setmp_noncritical auto true (fn () =>
    24.8 +  (Unsynchronized.setmp auto true (fn () =>
    24.9      Preferences.bool_pref auto
   24.10        "auto-solve" "Try to solve conjectures with existing theorems.") ());
   24.11  
    25.1 --- a/src/Tools/quickcheck.ML	Wed Sep 22 17:46:59 2010 +0200
    25.2 +++ b/src/Tools/quickcheck.ML	Wed Sep 22 18:21:48 2010 +0200
    25.3 @@ -42,7 +42,7 @@
    25.4  
    25.5  val _ =
    25.6    ProofGeneralPgip.add_preference Preferences.category_tracing
    25.7 -  (setmp_noncritical auto true (fn () =>
    25.8 +  (Unsynchronized.setmp auto true (fn () =>
    25.9      Preferences.bool_pref auto
   25.10        "auto-quickcheck"
   25.11        "Run Quickcheck automatically.") ());