# HG changeset patch
# User wenzelm
# Date 1384863231 -3600
# Node ID 2a7f9e79cb28a825db589393a7f53aed3d1371b8
# Parent  570ba266f5b548b78a80cb1a3408782fb8ddbf3c
proper theory name vs. node name;

diff -r 570ba266f5b5 -r 2a7f9e79cb28 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Nov 19 12:57:56 2013 +0100
+++ b/src/Pure/PIDE/document.ML	Tue Nov 19 13:13:51 2013 +0100
@@ -391,6 +391,11 @@
         Symtab.update (a, ())) all_visible all_required
   end;
 
+fun loaded_theory name =
+  (case try (unsuffix ".thy") name of
+    SOME a => Thy_Info.lookup_theory a
+  | NONE => NONE);
+
 fun init_theory deps node span =
   let
     (* FIXME provide files via Isabelle/Scala, not master_dir *)
@@ -402,7 +407,7 @@
     val imports = #imports header;
     val parents =
       imports |> map (fn (import, _) =>
-        (case Thy_Info.lookup_theory import of
+        (case loaded_theory import of
           SOME thy => thy
         | NONE =>
             Toplevel.end_theory (Position.file_only import)
@@ -413,7 +418,7 @@
   in Thy_Load.begin_theory master_dir header parents end;
 
 fun check_theory full name node =
-  is_some (Thy_Info.lookup_theory name) orelse
+  is_some (loaded_theory name) orelse
   can get_header node andalso (not full orelse is_some (get_result node));
 
 fun last_common state node_required node0 node =