src/Pure/library.ML
changeset 32737 76fa673eee8b
parent 32352 4839a704939a
child 32966 5b21661fe618
     1.1 --- a/src/Pure/library.ML	Mon Sep 28 23:51:13 2009 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Sep 29 11:48:32 2009 +0200
     1.3 @@ -57,13 +57,8 @@
     1.4    val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
     1.5    val exists: ('a -> bool) -> 'a list -> bool
     1.6    val forall: ('a -> bool) -> 'a list -> bool
     1.7 -  val set: bool ref -> bool
     1.8 -  val reset: bool ref -> bool
     1.9 -  val toggle: bool ref -> bool
    1.10 -  val change: 'a ref -> ('a -> 'a) -> unit
    1.11 -  val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b
    1.12 -  val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    1.13 -  val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    1.14 +  val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    1.15 +  val setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    1.16    val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
    1.17  
    1.18    (*lists*)
    1.19 @@ -123,8 +118,6 @@
    1.20    val suffixes: 'a list -> 'a list list
    1.21  
    1.22    (*integers*)
    1.23 -  val inc: int ref -> int
    1.24 -  val dec: int ref -> int
    1.25    val upto: int * int -> int list
    1.26    val downto: int * int -> int list
    1.27    val radixpand: int * int -> int list
    1.28 @@ -326,13 +319,6 @@
    1.29  
    1.30  (* flags *)
    1.31  
    1.32 -fun set flag = (flag := true; true);
    1.33 -fun reset flag = (flag := false; false);
    1.34 -fun toggle flag = (flag := not (! flag); ! flag);
    1.35 -
    1.36 -fun change r f = r := f (! r);
    1.37 -fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
    1.38 -
    1.39  (*temporarily set flag during execution*)
    1.40  fun setmp_noncritical flag value f x =
    1.41    uninterruptible (fn restore_attributes => fn () =>
    1.42 @@ -643,10 +629,6 @@
    1.43  
    1.44  (** integers **)
    1.45  
    1.46 -fun inc i = (i := ! i + (1: int); ! i);
    1.47 -fun dec i = (i := ! i - (1: int); ! i);
    1.48 -
    1.49 -
    1.50  (* lists of integers *)
    1.51  
    1.52  (*make the list [from, from + 1, ..., to]*)
    1.53 @@ -1055,7 +1037,7 @@
    1.54  local
    1.55    val a = 16807.0;
    1.56    val m = 2147483647.0;
    1.57 -  val random_seed = ref 1.0;
    1.58 +  val random_seed = Unsynchronized.ref 1.0;
    1.59  in
    1.60  
    1.61  fun random () = CRITICAL (fn () =>
    1.62 @@ -1121,17 +1103,18 @@
    1.63  val char_vec = Vector.tabulate (62, gensym_char);
    1.64  fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
    1.65  
    1.66 -val gensym_seed = ref (0: int);
    1.67 +val gensym_seed = Unsynchronized.ref (0: int);
    1.68  
    1.69  in
    1.70 -  fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed));
    1.71 +  fun gensym pre =
    1.72 +    pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed));
    1.73  end;
    1.74  
    1.75  
    1.76  (* stamps and serial numbers *)
    1.77  
    1.78 -type stamp = unit ref;
    1.79 -val stamp: unit -> stamp = ref;
    1.80 +type stamp = unit Unsynchronized.ref;
    1.81 +val stamp: unit -> stamp = Unsynchronized.ref;
    1.82  
    1.83  type serial = int;
    1.84  val serial = Multithreading.serial;