# HG changeset patch
# User wenzelm
# Date 1187385049 -7200
# Node ID 09b35593d0912c3b44679bb2b1793bde2ff2c5f4
# Parent  665b3ab2dabe37304cf9c6a76fdb2175aafa8270
updated generated file;

diff -r 665b3ab2dabe -r 09b35593d091 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Fri Aug 17 23:10:46 2007 +0200
+++ b/src/Tools/Metis/metis.ML	Fri Aug 17 23:10:49 2007 +0200
@@ -37,6 +37,12 @@
 
 val time : ('a -> 'b) -> 'a -> 'b
 
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing)                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val CRITICAL: (unit -> 'a) -> 'a
+
 end
 
 (**** Original file: PortableIsabelle.sml ****)
@@ -72,6 +78,12 @@
 
 val time = timeap;
 
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing)                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val CRITICAL = CRITICAL;
+
 end
 
 (* ------------------------------------------------------------------------- *)
@@ -1002,28 +1014,30 @@
 
 fun newgen () = newgenseed (Time.toReal (Time.now ()));
 
-fun random {seedref as ref seed} = 
-    (seedref := nextrand seed; seed / m);
-
-fun randomlist (n, {seedref as ref seed0}) = 
-    let fun h 0 seed res = (seedref := seed; res)
+fun random {seedref} = CRITICAL (fn () => 
+    (seedref := nextrand (! seedref); ! seedref / m));
+
+fun randomlist (n, {seedref}) = CRITICAL (fn () =>
+    let val seed0 = ! seedref
+        fun h 0 seed res = (seedref := seed; res)
 	  | h i seed res = h (i-1) (nextrand seed) (seed / m :: res)
-    in h n seed0 [] end;
+    in h n seed0 [] end);
 
 fun range (min, max) = 
     if min > max then raise Fail "Random.range: empty range" 
     else 
-	fn {seedref as ref seed} =>
-	(seedref := nextrand seed; min + (floor(real(max-min) * seed / m)));
+	fn {seedref} => CRITICAL (fn () =>
+	(seedref := nextrand (! seedref); min + (floor(real(max-min) * ! seedref / m))));
 
 fun rangelist (min, max) =
     if min > max then raise Fail "Random.rangelist: empty range" 
     else 
-	fn (n, {seedref as ref seed0}) => 
-	let fun h 0 seed res = (seedref := seed; res)
+	fn (n, {seedref}) => CRITICAL (fn () => 
+	let val seed0 = ! seedref
+            fun h 0 seed res = (seedref := seed; res)
 	      | h i seed res = h (i-1) (nextrand seed) 
 		               (min + floor(real(max-min) * seed / m) :: res)
-	in h n seed0 [] end
+	in h n seed0 [] end)
 
 end
 end;
@@ -1722,7 +1736,7 @@
 
   val primesList = ref (calcPrimes 10);
 in
-  fun primes n =
+  fun primes n = CRITICAL (fn () =>
       if length (!primesList) <= n then List.take (!primesList,n)
       else
         let
@@ -1730,9 +1744,9 @@
           val () = primesList := l
         in
           l
-        end;
-
-  fun primesUpTo n =
+        end);
+
+  fun primesUpTo n = CRITICAL (fn () =>
       let
         fun f k [] =
             let
@@ -1745,7 +1759,7 @@
             if p <= n then f (k + 1) ps else List.take (!primesList, k)
       in
         f 0 (!primesList)
-      end;
+      end);
 end;
 
 (* ------------------------------------------------------------------------- *)
@@ -1917,22 +1931,22 @@
 local
   val generator = ref 0
 in
-  fun newInt () =
+  fun newInt () = CRITICAL (fn () =>
       let
         val n = !generator
         val () = generator := n + 1
       in
         n
-      end;
+      end);
 
   fun newInts 0 = []
-    | newInts k =
+    | newInts k = CRITICAL (fn () =>
       let
         val n = !generator
         val () = generator := n + k
       in
         interval n k
-      end;
+      end);
 end;
 
 local
@@ -11127,14 +11141,14 @@
     let
       val counter : int NameMap.map ref = ref (NameMap.new ())
     in
-      fn n =>
+      fn n => CRITICAL (fn () =>
       let
         val ref m = counter
         val i = Option.getOpt (NameMap.peek m n, 0)
         val () = counter := NameMap.insert m (n, i + 1)
       in
         "skolem_" ^ n ^ (if i = 0 then "" else "_" ^ Int.toString i)
-      end
+      end)
     end;
 
 fun skolemize fv bv fm =
@@ -11325,13 +11339,13 @@
     let
       val counter : int ref = ref 0
     in
-      fn () =>
+      fn () => CRITICAL (fn () =>
       let
         val ref i = counter
         val () = counter := i + 1
       in
         "defCNF_" ^ Int.toString i
-      end
+      end)
     end;
 
 fun newDefinition def =
@@ -14831,7 +14845,8 @@
     let
       val r = ref 0
     in
-      fn () => case r of ref n => let val () = r := n + 1 in n end
+      fn () => CRITICAL (fn () =>
+        case r of ref n => let val () = r := n + 1 in n end)
     end;
 
 (* ------------------------------------------------------------------------- *)