src/Pure/PIDE/document.ML
changeset 44198 a41ea419de68
parent 44197 458573968568
child 44199 e38885e3ea60
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 15 16:38:42 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 15 19:27:55 2011 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4  fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
     1.5  fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
     1.6  
     1.7 -fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
     1.8 +fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result);
     1.9  fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
    1.10  
    1.11  val empty_exec = Lazy.value Toplevel.toplevel;
    1.12 @@ -322,8 +322,8 @@
    1.13      val exec' =
    1.14        Lazy.lazy (fn () =>
    1.15          let
    1.16 -          val tr = Toplevel.put_id (print_id exec_id') (Future.join command); (* FIXME Future.join_finished !? *)
    1.17 -          val st = Lazy.force exec;  (* FIXME Lazy.force_finished !? *)
    1.18 +          val tr = Toplevel.put_id (print_id exec_id') (Future.get_finished command);
    1.19 +          val st = Lazy.get_finished exec;
    1.20          in run_command node_info tr st end);
    1.21    in ((command_id, exec_id') :: assigns, (exec_id', exec') :: execs, exec') end;
    1.22