--- 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.
--- 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"];
--- 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",
--- 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"];
--- 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"];
--- 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"]);
+
--- 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.") ());
--- 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 =
--- 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;
--- 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
--- 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;
--- 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;
--- 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;
--- 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);
--- 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 **)
--- 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;
--- 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;
--- 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") (),
--- 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
--- 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);
--- 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
--- 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) =>
--- 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 () =>
--- 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.") ());
--- 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.") ());