src/Pure/PIDE/document.ML
changeset 47339 79bd24497ffd
parent 47336 bed4b2738d8a
child 47340 9bbf7fd96bcd
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Apr 04 17:21:39 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Apr 04 21:03:30 2012 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4    map_node (fn (touched, header, perspective, entries, _, result) =>
     1.5      (touched, header, perspective, entries, last_exec, result));
     1.6  
     1.7 -fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
     1.8 +fun get_result (Node {result, ...}) = result;
     1.9  fun set_result result =
    1.10    map_node (fn (touched, header, perspective, entries, last_exec, _) =>
    1.11      (touched, header, perspective, entries, last_exec, result));
    1.12 @@ -337,8 +337,9 @@
    1.13          (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
    1.14            SOME thy => thy
    1.15          | NONE =>
    1.16 -            get_theory (Position.file_only import)
    1.17 -              (snd (Future.join (the (AList.lookup (op =) deps import))))));
    1.18 +            Toplevel.end_theory (Position.file_only import)
    1.19 +              (Lazy.force
    1.20 +                (get_result (snd (Future.join (the (AList.lookup (op =) deps import))))))));
    1.21    in Thy_Load.begin_theory master_dir header parents end;
    1.22  
    1.23  fun check_theory nodes name =