explicit check of finished evaluation;

--- a/src/Pure/Concurrent/future.ML	Mon Aug 15 16:38:42 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Aug 15 19:27:55 2011 +0200
@@ -39,6 +39,7 @@
   val task_of: 'a future -> Task_Queue.task
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
+  val get_finished: 'a future -> 'a
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: Task_Queue.group -> unit
   val cancel: 'a future -> unit
@@ -105,6 +106,11 @@
 fun peek x = Single_Assignment.peek (result_of x);
 fun is_finished x = is_some (peek x);
 
+fun get_finished x =
+  (case peek x of
+    SOME res => Exn.release res
+  | NONE => raise Fail "Unfinished future evaluation");
+
 
 
 (** scheduling **)

--- a/src/Pure/Concurrent/lazy.ML	Mon Aug 15 16:38:42 2011 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Mon Aug 15 19:27:55 2011 +0200
@@ -10,6 +10,8 @@
 sig
   type 'a lazy
   val peek: 'a lazy -> 'a Exn.result option
+  val is_finished: 'a lazy -> bool
+  val get_finished: 'a lazy -> 'a
   val lazy: (unit -> 'a) -> 'a lazy
   val value: 'a -> 'a lazy
   val force_result: 'a lazy -> 'a Exn.result
@@ -36,6 +38,13 @@
 fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
 fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
 
+fun is_finished x = is_some (peek x);
+
+fun get_finished x =
+  (case peek x of
+    SOME res => Exn.release res
+  | NONE => raise Fail "Unfinished lazy evaluation");
+
 
 (* force result *)
 

--- a/src/Pure/Concurrent/lazy_sequential.ML	Mon Aug 15 16:38:42 2011 +0200
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Mon Aug 15 19:27:55 2011 +0200
@@ -25,6 +25,13 @@
 fun lazy e = Lazy (Unsynchronized.ref (Expr e));
 fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
 
+fun is_finished x = is_some (peek x);
+
+fun get_finished x =
+  (case peek x of
+    SOME res => Exn.release res
+  | NONE => raise Fail "Unfinished lazy evaluation");
+
 
 (* force result *)
 

--- a/src/Pure/PIDE/document.ML	Mon Aug 15 16:38:42 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Aug 15 19:27:55 2011 +0200
@@ -78,7 +78,7 @@
 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
 
-fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
+fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result);
 fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
 
 val empty_exec = Lazy.value Toplevel.toplevel;
@@ -322,8 +322,8 @@
     val exec' =
       Lazy.lazy (fn () =>
         let
-          val tr = Toplevel.put_id (print_id exec_id') (Future.join command); (* FIXME Future.join_finished !? *)
-          val st = Lazy.force exec;  (* FIXME Lazy.force_finished !? *)
+          val tr = Toplevel.put_id (print_id exec_id') (Future.get_finished command);
+          val st = Lazy.get_finished exec;
         in run_command node_info tr st end);
   in ((command_id, exec_id') :: assigns, (exec_id', exec') :: execs, exec') end;