added suspensions in Pure

--- a/src/HOL/Import/ImportRecorder.thy	Tue Sep 19 15:21:52 2006 +0200
+++ b/src/HOL/Import/ImportRecorder.thy	Tue Sep 19 15:21:55 2006 +0200
@@ -1,4 +1,4 @@
 theory ImportRecorder imports Main 
-uses  "seq.ML" "scan.ML" "mono_seq.ML" "mono_scan.ML" "susp.ML" "lazy_seq.ML" "xml.ML" "xmlconv.ML" "importrecorder.ML"
+uses  "seq.ML" "scan.ML" "mono_seq.ML" "mono_scan.ML" "lazy_seq.ML" "xml.ML" "xmlconv.ML" "importrecorder.ML"
 begin
 end
\ No newline at end of file

--- a/src/HOL/Import/lazy_seq.ML	Tue Sep 19 15:21:52 2006 +0200
+++ b/src/HOL/Import/lazy_seq.ML	Tue Sep 19 15:21:55 2006 +0200
@@ -82,7 +82,7 @@
 
 open Susp
 
-datatype 'a seq = Seq of ('a * 'a seq) option susp
+datatype 'a seq = Seq of ('a * 'a seq) option Susp.T
 
 exception Empty
 

--- a/src/HOL/Import/susp.ML	Tue Sep 19 15:21:52 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      HOL/Import/susp.ML
-    ID:         $Id$
-    Author:     Sebastian Skalberg, TU Muenchen
-
-Delayed evaluation.
-*)
-
-signature SUSP =
-sig
-
-type 'a susp
-
-val force : 'a susp -> 'a
-val delay : (unit -> 'a) -> 'a susp
-val value : 'a -> 'a susp
-
-end
-
-structure Susp :> SUSP =
-struct
-
-datatype 'a suspVal
-  = Value of 'a
-  | Delay of unit -> 'a
-
-type 'a susp = 'a suspVal ref
-
-fun force (ref (Value v)) = v
-  | force (r as ref (Delay f)) =
-    let
-	val v = f ()
-    in
-	r := Value v;
-	v
-    end
-
-fun delay f = ref (Delay f)
-
-fun value v = ref (Value v)
-
-end

--- a/src/Pure/General/ROOT.ML	Tue Sep 19 15:21:52 2006 +0200
+++ b/src/Pure/General/ROOT.ML	Tue Sep 19 15:21:55 2006 +0200
@@ -17,6 +17,7 @@
 use "name_space.ML";
 use "name_mangler.ML";
 use "seq.ML";
+use "susp.ML";
 use "rat.ML";
 use "position.ML";
 use "path.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/susp.ML	Tue Sep 19 15:21:55 2006 +0200
@@ -0,0 +1,45 @@
+(*  Title:      Pure/General/susp.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg and Florian Haftmann, TU Muenchen
+
+Delayed evaluation.
+*)
+
+signature SUSP =
+sig
+  type 'a T
+  val value: 'a -> 'a T
+  val delay: (unit -> 'a) -> 'a T
+  val force: 'a T -> 'a
+  val peek: 'a T -> 'a option
+  val same: 'a T * 'a T -> bool
+end
+
+structure Susp : SUSP =
+struct
+
+datatype 'a susp =
+    Value of 'a
+  | Delay of unit -> 'a;
+
+type 'a T = 'a susp ref;
+
+fun value v = ref (Value v);
+
+fun delay f = ref (Delay f);
+
+fun force (ref (Value v)) = v
+  | force (r as ref (Delay f)) =
+      let
+        val v = f ()
+      in
+        r := Value v;
+        v
+      end;
+
+fun peek (ref (Value v)) = SOME v
+  | peek (ref (Delay _)) = NONE;
+
+fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)
+
+end