1.1 --- a/src/Pure/PIDE/document.ML	Tue Nov 19 12:57:56 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Nov 19 13:13:51 2013 +0100
     1.3 @@ -391,6 +391,11 @@
     1.4          Symtab.update (a, ())) all_visible all_required
     1.5    end;
     1.6  
     1.7 +fun loaded_theory name =
     1.8 +  (case try (unsuffix ".thy") name of
     1.9 +    SOME a => Thy_Info.lookup_theory a
    1.10 +  | NONE => NONE);
    1.11 +
    1.12  fun init_theory deps node span =
    1.13    let
    1.14      (* FIXME provide files via Isabelle/Scala, not master_dir *)
    1.15 @@ -402,7 +407,7 @@
    1.16      val imports = #imports header;
    1.17      val parents =
    1.18        imports |> map (fn (import, _) =>
    1.19 -        (case Thy_Info.lookup_theory import of
    1.20 +        (case loaded_theory import of
    1.21            SOME thy => thy
    1.22          | NONE =>
    1.23              Toplevel.end_theory (Position.file_only import)
    1.24 @@ -413,7 +418,7 @@
    1.25    in Thy_Load.begin_theory master_dir header parents end;
    1.26  
    1.27  fun check_theory full name node =
    1.28 -  is_some (Thy_Info.lookup_theory name) orelse
    1.29 +  is_some (loaded_theory name) orelse
    1.30    can get_header node andalso (not full orelse is_some (get_result node));
    1.31  
    1.32  fun last_common state node_required node0 node =