# HG changeset patch
# User wenzelm
# Date 1285172508 -7200
# Node ID 8052101883c310cd04934a51aaa831e93cdb0219
# Parent  b926f8ec9cacaa3f5b07626b79596cfc946cdfc7
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;

diff -r b926f8ec9cac -r 8052101883c3 NEWS
--- a/NEWS	Wed Sep 22 17:46:59 2010 +0200
+++ b/NEWS	Wed Sep 22 18:21:48 2010 +0200
@@ -244,6 +244,9 @@
 
 *** ML ***
 
+* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
+meaning.
+
 * Renamed structure PureThy to Pure_Thy and moved most of its
 operations to structure Global_Theory, to emphasize that this is
 rarely-used global-only stuff.
diff -r b926f8ec9cac -r 8052101883c3 src/HOL/Import/HOL/ROOT.ML
--- a/src/HOL/Import/HOL/ROOT.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/HOL/Import/HOL/ROOT.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -1,2 +1,2 @@
 use_thy "~~/src/HOL/Old_Number_Theory/Primes";
-setmp_noncritical quick_and_dirty true use_thys ["HOL4Prob", "HOL4"];
+Unsynchronized.setmp quick_and_dirty true use_thys ["HOL4Prob", "HOL4"];
diff -r b926f8ec9cac -r 8052101883c3 src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/HOL/Induct/ROOT.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -1,4 +1,4 @@
-setmp_noncritical quick_and_dirty true
+Unsynchronized.setmp quick_and_dirty true
   use_thys ["Common_Patterns"];
 
 use_thys ["QuoDataType", "QuoNestedDataType", "Term", "SList",
diff -r b926f8ec9cac -r 8052101883c3 src/HOL/Nitpick_Examples/ROOT.ML
--- a/src/HOL/Nitpick_Examples/ROOT.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/HOL/Nitpick_Examples/ROOT.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -5,4 +5,4 @@
 Nitpick examples.
 *)
 
-setmp_noncritical quick_and_dirty true use_thys ["Nitpick_Examples"];
+Unsynchronized.setmp quick_and_dirty true use_thys ["Nitpick_Examples"];
diff -r b926f8ec9cac -r 8052101883c3 src/HOL/Nominal/Examples/ROOT.ML
--- a/src/HOL/Nominal/Examples/ROOT.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -1,3 +1,3 @@
 use_thys ["Nominal_Examples"];
 
-setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"]; 
+Unsynchronized.setmp quick_and_dirty true use_thys ["VC_Condition"];
diff -r b926f8ec9cac -r 8052101883c3 src/HOL/Predicate_Compile_Examples/ROOT.ML
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -1,5 +1,20 @@
-use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples", "IMP_1", "IMP_2", "IMP_3", "IMP_4"];
+use_thys [
+  "Predicate_Compile_Examples",
+  "Predicate_Compile_Quickcheck_Examples",
+  "Specialisation_Examples",
+  "IMP_1",
+  "IMP_2",
+  "IMP_3",
+  "IMP_4"];
+
 if getenv "EXEC_SWIPL" = "" andalso getenv "EXEC_YAP" = "" then
-  (warning "No prolog system found - could not use example theories that require a prolog system"; ())
+  (warning "No prolog system found - skipping some example theories"; ())
 else
-  (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"])
+  (use_thys [
+    "Code_Prolog_Examples",
+    "Context_Free_Grammar_Example",
+    "Hotel_Example",
+    "Lambda_Example",
+    "List_Examples"];
+   Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"]);
+
diff -r b926f8ec9cac -r 8052101883c3 src/HOL/Tools/try.ML
--- a/src/HOL/Tools/try.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/HOL/Tools/try.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -18,7 +18,7 @@
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
-  (setmp_noncritical auto true (fn () =>
+  (Unsynchronized.setmp auto true (fn () =>
     Preferences.bool_pref auto
       "auto-try" "Try standard proof methods.") ());
 
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -976,7 +976,7 @@
       else ();
     val test_proof =
       try (local_skip_proof true)
-      |> setmp_noncritical testing true
+      |> Unsynchronized.setmp testing true
       |> Exn.capture;
 
     fun after_qed' results =
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -14,7 +14,7 @@
 sig
   include BASIC_MULTITHREADING
   val available: bool
-  val max_threads: int Unsynchronized.ref
+  val max_threads: int ref
   val max_threads_value: unit -> int
   val enabled: unit -> bool
   val no_interrupts: Thread.threadAttribute list
@@ -24,7 +24,7 @@
   val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
   val sync_wait: Thread.threadAttribute list option -> Time.time option ->
     ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
-  val trace: int Unsynchronized.ref
+  val trace: int ref
   val tracing: int -> (unit -> string) -> unit
   val tracing_time: bool -> Time.time -> (unit -> string) -> unit
   val real_time: ('a -> unit) -> 'a -> Time.time
@@ -38,7 +38,7 @@
 (* options *)
 
 val available = false;
-val max_threads = Unsynchronized.ref (1: int);
+val max_threads = ref (1: int);
 fun max_threads_value () = 1: int;
 fun enabled () = false;
 
@@ -57,7 +57,7 @@
 
 (* tracing *)
 
-val trace = Unsynchronized.ref (0: int);
+val trace = ref (0: int);
 fun tracing _ _ = ();
 fun tracing_time _ _ _ = ();
 fun real_time f x = (f x; Time.zeroTime);
@@ -72,7 +72,7 @@
 
 (* serial numbers *)
 
-local val count = Unsynchronized.ref (0: int)
+local val count = ref (0: int)
 in fun serial () = (count := ! count + 1; ! count) end;
 
 end;
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -31,7 +31,7 @@
 
 val available = true;
 
-val max_threads = Unsynchronized.ref 0;
+val max_threads = ref 0;
 
 fun max_threads_value () =
   let val m = ! max_threads in
@@ -109,7 +109,7 @@
 
 (* tracing *)
 
-val trace = Unsynchronized.ref 0;
+val trace = ref 0;
 
 fun tracing level msg =
   if level > ! trace then ()
@@ -143,7 +143,7 @@
 fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
   let
     val worker = Thread.self ();
-    val timeout = Unsynchronized.ref false;
+    val timeout = ref false;
     val watchdog = Thread.fork (fn () =>
       (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
 
@@ -168,7 +168,7 @@
 
     (*result state*)
     datatype result = Wait | Signal | Result of int;
-    val result = Unsynchronized.ref Wait;
+    val result = ref Wait;
     val lock = Mutex.mutex ();
     val cond = ConditionVar.conditionVar ();
     fun set_result res =
@@ -226,8 +226,8 @@
 local
 
 val critical_lock = Mutex.mutex ();
-val critical_thread = Unsynchronized.ref (NONE: Thread.thread option);
-val critical_name = Unsynchronized.ref "";
+val critical_thread = ref (NONE: Thread.thread option);
+val critical_name = ref "";
 
 in
 
@@ -269,7 +269,7 @@
 local
 
 val serial_lock = Mutex.mutex ();
-val serial_count = Unsynchronized.ref 0;
+val serial_count = ref 0;
 
 in
 
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/polyml-5.2.1.ML
--- a/src/Pure/ML-Systems/polyml-5.2.1.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/ML-Systems/polyml-5.2.1.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -3,8 +3,6 @@
 Compatibility wrapper for Poly/ML 5.2.1.
 *)
 
-use "ML-Systems/unsynchronized.ML";
-
 open Thread;
 
 structure ML_Name_Space =
@@ -18,6 +16,10 @@
 
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/multithreading_polyml.ML";
+use "ML-Systems/unsynchronized.ML";
+
+val _ = PolyML.Compiler.forgetValue "ref";
+val _ = PolyML.Compiler.forgetType "ref";
 
 val pointer_eq = PolyML.pointerEq;
 
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/polyml-5.2.ML
--- a/src/Pure/ML-Systems/polyml-5.2.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/ML-Systems/polyml-5.2.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -3,8 +3,6 @@
 Compatibility wrapper for Poly/ML 5.2.
 *)
 
-use "ML-Systems/unsynchronized.ML";
-
 open Thread;
 
 structure ML_Name_Space =
@@ -17,9 +15,12 @@
 fun reraise exn = raise exn;
 
 use "ML-Systems/polyml_common.ML";
-
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
+use "ML-Systems/unsynchronized.ML";
+
+val _ = PolyML.Compiler.forgetValue "ref";
+val _ = PolyML.Compiler.forgetType "ref";
 
 val pointer_eq = PolyML.pointerEq;
 
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -3,8 +3,6 @@
 Compatibility wrapper for Poly/ML 5.3 and 5.4.
 *)
 
-use "ML-Systems/unsynchronized.ML";
-
 open Thread;
 
 structure ML_Name_Space =
@@ -21,6 +19,10 @@
 
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/multithreading_polyml.ML";
+use "ML-Systems/unsynchronized.ML";
+
+val _ = PolyML.Compiler.forgetValue "ref";
+val _ = PolyML.Compiler.forgetType "ref";
 
 val pointer_eq = PolyML.pointerEq;
 
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -29,8 +29,6 @@
 val _ = PolyML.Compiler.forgetValue "foldl";
 val _ = PolyML.Compiler.forgetValue "foldr";
 val _ = PolyML.Compiler.forgetValue "print";
-val _ = PolyML.Compiler.forgetValue "ref";
-val _ = PolyML.Compiler.forgetType "ref";
 
 
 (* Compiler options *)
@@ -62,7 +60,7 @@
 (* toplevel printing *)
 
 local
-  val depth = Unsynchronized.ref 10;
+  val depth = ref 10;
 in
   fun get_print_depth () = ! depth;
   fun print_depth n = (depth := n; PolyML.print_depth n);
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -7,7 +7,6 @@
 fun reraise exn = raise exn;
 
 use "ML-Systems/proper_int.ML";
-use "ML-Systems/unsynchronized.ML";
 use "ML-Systems/overloading_smlnj.ML";
 use "General/exn.ML";
 use "ML-Systems/single_assignment.ML";
@@ -159,6 +158,9 @@
 end;
 
 
+use "ML-Systems/unsynchronized.ML";
+
+
 
 (** OS related **)
 
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/thread_dummy.ML
--- a/src/Pure/ML-Systems/thread_dummy.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/ML-Systems/thread_dummy.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -60,7 +60,7 @@
 
 local
 
-val data = Unsynchronized.ref ([]: Universal.universal  Unsynchronized.ref list);
+val data = ref ([]: Universal.universal  ref list);
 
 fun find_data tag =
   let
@@ -75,7 +75,7 @@
 fun setLocal (tag, x) =
   (case find_data tag of
     SOME r => r := Universal.tagInject tag x
-  | NONE => data :=  Unsynchronized.ref (Universal.tagInject tag x) :: ! data);
+  | NONE => data :=  ref (Universal.tagInject tag x) :: ! data);
 
 end;
 end;
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ML-Systems/unsynchronized.ML
--- a/src/Pure/ML-Systems/unsynchronized.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/ML-Systems/unsynchronized.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -18,4 +18,13 @@
 fun inc i = (i := ! i + (1: int); ! i);
 fun dec i = (i := ! i - (1: int); ! i);
 
+fun setmp flag value f x =
+  uninterruptible (fn restore_attributes => fn () =>
+    let
+      val orig_value = ! flag;
+      val _ = flag := value;
+      val result = Exn.capture (restore_attributes f) x;
+      val _ = flag := orig_value;
+    in Exn.release result end) ();
+
 end;
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -78,7 +78,7 @@
 
 (* preferences of Pure *)
 
-val proof_pref = setmp_noncritical Proofterm.proofs 1 (fn () =>
+val proof_pref = Unsynchronized.setmp 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);
@@ -164,7 +164,7 @@
   thm_deps_pref];
 
 val proof_preferences =
- [setmp_noncritical quick_and_dirty true (fn () =>
+ [Unsynchronized.setmp quick_and_dirty true (fn () =>
     bool_pref quick_and_dirty
       "quick-and-dirty"
       "Take a few short cuts") (),
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -1044,7 +1044,7 @@
    This works for preferences but not generally guaranteed
    because we haven't done full setup here (e.g., no pgml mode)  *)
 fun process_pgip_emacs str =
-     setmp_noncritical output_xml_fn (!pgip_output_channel) process_pgip_plain str
+     Unsynchronized.setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str
 
 end
 
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/System/session.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -110,11 +110,11 @@
         in () end
       else use root;
       finish ()))
-    |> setmp_noncritical Proofterm.proofs level
-    |> setmp_noncritical print_mode (modes @ print_mode_value ())
-    |> setmp_noncritical Goal.parallel_proofs parallel_proofs
-    |> setmp_noncritical Multithreading.trace trace_threads
-    |> setmp_noncritical Multithreading.max_threads
+    |> Unsynchronized.setmp Proofterm.proofs level
+    |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
+    |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
+    |> Unsynchronized.setmp Multithreading.trace trace_threads
+    |> Unsynchronized.setmp Multithreading.max_threads
       (if Multithreading.available then max_threads
        else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
   handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/Thy/html.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -277,7 +277,7 @@
 (* document *)
 
 val charset = Unsynchronized.ref "ISO-8859-1";
-fun with_charset s = setmp_noncritical charset s;   (* FIXME unreliable *)
+fun with_charset s = Unsynchronized.setmp charset s;   (* FIXME unreliable *)
 
 fun begin_document title =
   let val cs = ! charset in
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/Thy/present.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -165,7 +165,7 @@
   CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
 
 val suppress_tex_source = Unsynchronized.ref false;
-fun no_document f x = setmp_noncritical suppress_tex_source true f x;
+fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x;  (* FIXME unreliable *)
 
 fun init_theory_info name info =
   change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
diff -r b926f8ec9cac -r 8052101883c3 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Pure/library.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -56,7 +56,6 @@
   val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
   val exists: ('a -> bool) -> 'a list -> bool
   val forall: ('a -> bool) -> 'a list -> bool
-  val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
   val setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
   val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
 
@@ -306,18 +305,8 @@
 
 (* flags *)
 
-(*temporarily set flag during execution*)
-fun setmp_noncritical flag value f x =
-  uninterruptible (fn restore_attributes => fn () =>
-    let
-      val orig_value = ! flag;
-      val _ = flag := value;
-      val result = Exn.capture (restore_attributes f) x;
-      val _ = flag := orig_value;
-    in Exn.release result end) ();
-
 fun setmp_CRITICAL flag value f x =
-  NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x);
+  NAMED_CRITICAL "setmp" (fn () => Unsynchronized.setmp flag value f x);
 
 fun setmp_thread_data tag orig_data data f x =
   uninterruptible (fn restore_attributes => fn () =>
diff -r b926f8ec9cac -r 8052101883c3 src/Tools/auto_solve.ML
--- a/src/Tools/auto_solve.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Tools/auto_solve.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -25,7 +25,7 @@
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
-  (setmp_noncritical auto true (fn () =>
+  (Unsynchronized.setmp auto true (fn () =>
     Preferences.bool_pref auto
       "auto-solve" "Try to solve conjectures with existing theorems.") ());
 
diff -r b926f8ec9cac -r 8052101883c3 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Sep 22 17:46:59 2010 +0200
+++ b/src/Tools/quickcheck.ML	Wed Sep 22 18:21:48 2010 +0200
@@ -42,7 +42,7 @@
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
-  (setmp_noncritical auto true (fn () =>
+  (Unsynchronized.setmp auto true (fn () =>
     Preferences.bool_pref auto
       "auto-quickcheck"
       "Run Quickcheck automatically.") ());