1.1 --- a/src/Pure/IsaMakefile Mon Sep 28 23:51:13 2009 +0200
1.2 +++ b/src/Pure/IsaMakefile Tue Sep 29 11:48:32 2009 +0200
1.3 @@ -32,7 +32,7 @@
1.4 ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
1.5 ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
1.6 ML-Systems/timing.ML ML-Systems/time_limit.ML \
1.7 - ML-Systems/universal.ML
1.8 + ML-Systems/universal.ML ML-Systems/unsynchronized.ML
1.9
1.10 RAW: $(OUT)/RAW
1.11
2.1 --- a/src/Pure/ML-Systems/mosml.ML Mon Sep 28 23:51:13 2009 +0200
2.2 +++ b/src/Pure/ML-Systems/mosml.ML Tue Sep 29 11:48:32 2009 +0200
2.3 @@ -41,6 +41,7 @@
2.4 fun reraise exn = raise exn;
2.5
2.6 use "ML-Systems/exn.ML";
2.7 +use "ML-Systems/unsynchronized.ML";
2.8 use "ML-Systems/universal.ML";
2.9 use "ML-Systems/thread_dummy.ML";
2.10 use "ML-Systems/multithreading.ML";
3.1 --- a/src/Pure/ML-Systems/polyml_common.ML Mon Sep 28 23:51:13 2009 +0200
3.2 +++ b/src/Pure/ML-Systems/polyml_common.ML Tue Sep 29 11:48:32 2009 +0200
3.3 @@ -6,6 +6,7 @@
3.4 exception Interrupt = SML90.Interrupt;
3.5
3.6 use "ML-Systems/exn.ML";
3.7 +use "ML-Systems/unsynchronized.ML";
3.8 use "ML-Systems/multithreading.ML";
3.9 use "ML-Systems/time_limit.ML";
3.10 use "ML-Systems/timing.ML";
3.11 @@ -50,7 +51,7 @@
3.12 (* print depth *)
3.13
3.14 local
3.15 - val depth = ref 10;
3.16 + val depth = Unsynchronized.ref 10;
3.17 in
3.18 fun get_print_depth () = ! depth;
3.19 fun print_depth n = (depth := n; PolyML.print_depth n);
4.1 --- a/src/Pure/ML-Systems/smlnj.ML Mon Sep 28 23:51:13 2009 +0200
4.2 +++ b/src/Pure/ML-Systems/smlnj.ML Tue Sep 29 11:48:32 2009 +0200
4.3 @@ -9,6 +9,7 @@
4.4 use "ML-Systems/proper_int.ML";
4.5 use "ML-Systems/overloading_smlnj.ML";
4.6 use "ML-Systems/exn.ML";
4.7 +use "ML-Systems/unsynchronized.ML";
4.8 use "ML-Systems/universal.ML";
4.9 use "ML-Systems/thread_dummy.ML";
4.10 use "ML-Systems/multithreading.ML";
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Pure/ML-Systems/unsynchronized.ML Tue Sep 29 11:48:32 2009 +0200
5.3 @@ -0,0 +1,25 @@
5.4 +(* Title: Pure/ML-Systems/unsynchronized.ML
5.5 + Author: Makarius
5.6 +
5.7 +Raw ML references as unsynchronized state variables.
5.8 +*)
5.9 +
5.10 +structure Unsynchronized =
5.11 +struct
5.12 +
5.13 +datatype ref = datatype ref;
5.14 +
5.15 +val op := = op :=;
5.16 +val ! = !;
5.17 +
5.18 +fun set flag = (flag := true; true);
5.19 +fun reset flag = (flag := false; false);
5.20 +fun toggle flag = (flag := not (! flag); ! flag);
5.21 +
5.22 +fun change r f = r := f (! r);
5.23 +fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
5.24 +
5.25 +fun inc i = (i := ! i + (1: int); ! i);
5.26 +fun dec i = (i := ! i - (1: int); ! i);
5.27 +
5.28 +end;
6.1 --- a/src/Pure/library.ML Mon Sep 28 23:51:13 2009 +0200
6.2 +++ b/src/Pure/library.ML Tue Sep 29 11:48:32 2009 +0200
6.3 @@ -57,13 +57,8 @@
6.4 val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
6.5 val exists: ('a -> bool) -> 'a list -> bool
6.6 val forall: ('a -> bool) -> 'a list -> bool
6.7 - val set: bool ref -> bool
6.8 - val reset: bool ref -> bool
6.9 - val toggle: bool ref -> bool
6.10 - val change: 'a ref -> ('a -> 'a) -> unit
6.11 - val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b
6.12 - val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
6.13 - val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
6.14 + val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
6.15 + val setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
6.16 val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
6.17
6.18 (*lists*)
6.19 @@ -123,8 +118,6 @@
6.20 val suffixes: 'a list -> 'a list list
6.21
6.22 (*integers*)
6.23 - val inc: int ref -> int
6.24 - val dec: int ref -> int
6.25 val upto: int * int -> int list
6.26 val downto: int * int -> int list
6.27 val radixpand: int * int -> int list
6.28 @@ -326,13 +319,6 @@
6.29
6.30 (* flags *)
6.31
6.32 -fun set flag = (flag := true; true);
6.33 -fun reset flag = (flag := false; false);
6.34 -fun toggle flag = (flag := not (! flag); ! flag);
6.35 -
6.36 -fun change r f = r := f (! r);
6.37 -fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
6.38 -
6.39 (*temporarily set flag during execution*)
6.40 fun setmp_noncritical flag value f x =
6.41 uninterruptible (fn restore_attributes => fn () =>
6.42 @@ -643,10 +629,6 @@
6.43
6.44 (** integers **)
6.45
6.46 -fun inc i = (i := ! i + (1: int); ! i);
6.47 -fun dec i = (i := ! i - (1: int); ! i);
6.48 -
6.49 -
6.50 (* lists of integers *)
6.51
6.52 (*make the list [from, from + 1, ..., to]*)
6.53 @@ -1055,7 +1037,7 @@
6.54 local
6.55 val a = 16807.0;
6.56 val m = 2147483647.0;
6.57 - val random_seed = ref 1.0;
6.58 + val random_seed = Unsynchronized.ref 1.0;
6.59 in
6.60
6.61 fun random () = CRITICAL (fn () =>
6.62 @@ -1121,17 +1103,18 @@
6.63 val char_vec = Vector.tabulate (62, gensym_char);
6.64 fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
6.65
6.66 -val gensym_seed = ref (0: int);
6.67 +val gensym_seed = Unsynchronized.ref (0: int);
6.68
6.69 in
6.70 - fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed));
6.71 + fun gensym pre =
6.72 + pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed));
6.73 end;
6.74
6.75
6.76 (* stamps and serial numbers *)
6.77
6.78 -type stamp = unit ref;
6.79 -val stamp: unit -> stamp = ref;
6.80 +type stamp = unit Unsynchronized.ref;
6.81 +val stamp: unit -> stamp = Unsynchronized.ref;
6.82
6.83 type serial = int;
6.84 val serial = Multithreading.serial;