Raw ML references as unsynchronized state variables.

--- a/src/Pure/IsaMakefile	Mon Sep 28 23:51:13 2009 +0200
+++ b/src/Pure/IsaMakefile	Tue Sep 29 11:48:32 2009 +0200
@@ -32,7 +32,7 @@
   ML-Systems/pp_polyml.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML	\
   ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML			\
   ML-Systems/timing.ML ML-Systems/time_limit.ML				\
-  ML-Systems/universal.ML
+  ML-Systems/universal.ML ML-Systems/unsynchronized.ML
 
 RAW: $(OUT)/RAW
 

--- a/src/Pure/ML-Systems/mosml.ML	Mon Sep 28 23:51:13 2009 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Tue Sep 29 11:48:32 2009 +0200
@@ -41,6 +41,7 @@
 fun reraise exn = raise exn;
 
 use "ML-Systems/exn.ML";
+use "ML-Systems/unsynchronized.ML";
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";

--- a/src/Pure/ML-Systems/polyml_common.ML	Mon Sep 28 23:51:13 2009 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Tue Sep 29 11:48:32 2009 +0200
@@ -6,6 +6,7 @@
 exception Interrupt = SML90.Interrupt;
 
 use "ML-Systems/exn.ML";
+use "ML-Systems/unsynchronized.ML";
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
 use "ML-Systems/timing.ML";
@@ -50,7 +51,7 @@
 (* print depth *)
 
 local
-  val depth = ref 10;
+  val depth = Unsynchronized.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	Mon Sep 28 23:51:13 2009 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Tue Sep 29 11:48:32 2009 +0200
@@ -9,6 +9,7 @@
 use "ML-Systems/proper_int.ML";
 use "ML-Systems/overloading_smlnj.ML";
 use "ML-Systems/exn.ML";
+use "ML-Systems/unsynchronized.ML";
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/unsynchronized.ML	Tue Sep 29 11:48:32 2009 +0200
@@ -0,0 +1,25 @@
+(*  Title:      Pure/ML-Systems/unsynchronized.ML
+    Author:     Makarius
+
+Raw ML references as unsynchronized state variables.
+*)
+
+structure Unsynchronized =
+struct
+
+datatype ref = datatype ref;
+
+val op := = op :=;
+val ! = !;
+
+fun set flag = (flag := true; true);
+fun reset flag = (flag := false; false);
+fun toggle flag = (flag := not (! flag); ! flag);
+
+fun change r f = r := f (! r);
+fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
+
+fun inc i = (i := ! i + (1: int); ! i);
+fun dec i = (i := ! i - (1: int); ! i);
+
+end;

--- a/src/Pure/library.ML	Mon Sep 28 23:51:13 2009 +0200
+++ b/src/Pure/library.ML	Tue Sep 29 11:48:32 2009 +0200
@@ -57,13 +57,8 @@
   val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
   val exists: ('a -> bool) -> 'a list -> bool
   val forall: ('a -> bool) -> 'a list -> bool
-  val set: bool ref -> bool
-  val reset: bool ref -> bool
-  val toggle: bool ref -> bool
-  val change: 'a ref -> ('a -> 'a) -> unit
-  val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b
-  val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
-  val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+  val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+  val setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
   val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
 
   (*lists*)
@@ -123,8 +118,6 @@
   val suffixes: 'a list -> 'a list list
 
   (*integers*)
-  val inc: int ref -> int
-  val dec: int ref -> int
   val upto: int * int -> int list
   val downto: int * int -> int list
   val radixpand: int * int -> int list
@@ -326,13 +319,6 @@
 
 (* flags *)
 
-fun set flag = (flag := true; true);
-fun reset flag = (flag := false; false);
-fun toggle flag = (flag := not (! flag); ! flag);
-
-fun change r f = r := f (! r);
-fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
-
 (*temporarily set flag during execution*)
 fun setmp_noncritical flag value f x =
   uninterruptible (fn restore_attributes => fn () =>
@@ -643,10 +629,6 @@
 
 (** integers **)
 
-fun inc i = (i := ! i + (1: int); ! i);
-fun dec i = (i := ! i - (1: int); ! i);
-
-
 (* lists of integers *)
 
 (*make the list [from, from + 1, ..., to]*)
@@ -1055,7 +1037,7 @@
 local
   val a = 16807.0;
   val m = 2147483647.0;
-  val random_seed = ref 1.0;
+  val random_seed = Unsynchronized.ref 1.0;
 in
 
 fun random () = CRITICAL (fn () =>
@@ -1121,17 +1103,18 @@
 val char_vec = Vector.tabulate (62, gensym_char);
 fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
 
-val gensym_seed = ref (0: int);
+val gensym_seed = Unsynchronized.ref (0: int);
 
 in
-  fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed));
+  fun gensym pre =
+    pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed));
 end;
 
 
 (* stamps and serial numbers *)
 
-type stamp = unit ref;
-val stamp: unit -> stamp = ref;
+type stamp = unit Unsynchronized.ref;
+val stamp: unit -> stamp = Unsynchronized.ref;
 
 type serial = int;
 val serial = Multithreading.serial;