tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;

--- a/src/Pure/PIDE/document.ML	Wed Apr 04 17:21:39 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Apr 04 21:03:30 2012 +0200
@@ -127,7 +127,7 @@
   map_node (fn (touched, header, perspective, entries, _, result) =>
     (touched, header, perspective, entries, last_exec, result));
 
-fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
+fun get_result (Node {result, ...}) = result;
 fun set_result result =
   map_node (fn (touched, header, perspective, entries, last_exec, _) =>
     (touched, header, perspective, entries, last_exec, result));
@@ -337,8 +337,9 @@
         (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
           SOME thy => thy
         | NONE =>
-            get_theory (Position.file_only import)
-              (snd (Future.join (the (AList.lookup (op =) deps import))))));
+            Toplevel.end_theory (Position.file_only import)
+              (Lazy.force
+                (get_result (snd (Future.join (the (AList.lookup (op =) deps import))))))));
   in Thy_Load.begin_theory master_dir header parents end;
 
 fun check_theory nodes name =