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 =