# HG changeset patch # User wenzelm # Date 1313429275 -7200 # Node ID a41ea419de68b582ab183626bdd37c26067d2ec5 # Parent 4585739685681f75632555e9e8521ca9874d2cf7 explicit check of finished evaluation; diff -r 458573968568 -r a41ea419de68 src/Pure/Concurrent/future.ML --- 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 **) diff -r 458573968568 -r a41ea419de68 src/Pure/Concurrent/lazy.ML --- 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 *) diff -r 458573968568 -r a41ea419de68 src/Pure/Concurrent/lazy_sequential.ML --- 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 *) diff -r 458573968568 -r a41ea419de68 src/Pure/PIDE/document.ML --- 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;