--- a/src/Pure/Concurrent/random.ML Thu Mar 10 09:50:53 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(* Title: Pure/Concurrent/random.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
-
-Pseudo random numbers.
-*)
-
-signature RANDOM =
-sig
- val random: unit -> real
- exception RANDOM
- val random_range: int -> int -> int
-end;
-
-structure Random: RANDOM =
-struct
-
-fun rmod x y = x - y * Real.realFloor (x / y);
-
-local
- val a = 16807.0;
- val m = 2147483647.0;
- val random_seed = Synchronized.var "random_seed" 1.0;
-in
-
-fun random () =
- Synchronized.change_result random_seed
- (fn r => let val r' = rmod (a * r) m in (r', r') end);
-
-end;
-
-exception RANDOM;
-
-fun random_range l h =
- if h < l orelse l < 0 then raise RANDOM
- else l + Real.floor (rmod (random ()) (real (h - l + 1)));
-
-end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/random.ML Thu Mar 10 09:56:29 2016 +0100
@@ -0,0 +1,38 @@
+(* Title: Pure/General/random.ML
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Pseudo random numbers.
+*)
+
+signature RANDOM =
+sig
+ val random: unit -> real
+ exception RANDOM
+ val random_range: int -> int -> int
+end;
+
+structure Random: RANDOM =
+struct
+
+fun rmod x y = x - y * Real.realFloor (x / y);
+
+local
+ val a = 16807.0;
+ val m = 2147483647.0;
+ val random_seed = Synchronized.var "random_seed" 1.0;
+in
+
+fun random () =
+ Synchronized.change_result random_seed
+ (fn r => let val r' = rmod (a * r) m in (r', r') end);
+
+end;
+
+exception RANDOM;
+
+fun random_range l h =
+ if h < l orelse l < 0 then raise RANDOM
+ else l + Real.floor (rmod (random ()) (real (h - l + 1)));
+
+end;
+
--- a/src/Pure/ROOT Thu Mar 10 09:50:53 2016 +0100
+++ b/src/Pure/ROOT Thu Mar 10 09:56:29 2016 +0100
@@ -12,7 +12,6 @@
"Concurrent/multithreading.ML"
"Concurrent/par_exn.ML"
"Concurrent/par_list.ML"
- "Concurrent/random.ML"
"Concurrent/single_assignment.ML"
"Concurrent/standard_thread.ML"
"Concurrent/synchronized.ML"
@@ -45,6 +44,7 @@
"General/print_mode.ML"
"General/properties.ML"
"General/queue.ML"
+ "General/random.ML"
"General/same.ML"
"General/scan.ML"
"General/secure.ML"
--- a/src/Pure/ROOT.ML Thu Mar 10 09:50:53 2016 +0100
+++ b/src/Pure/ROOT.ML Thu Mar 10 09:56:29 2016 +0100
@@ -107,8 +107,8 @@
use "Concurrent/synchronized.ML";
use "Concurrent/counter.ML";
-use "Concurrent/random.ML";
+use "General/random.ML";
use "General/properties.ML";
use "General/output.ML";
use "PIDE/markup.ML";