src/Pure/PIDE/resources.scala
changeset 65357 9a2c266f97c8
parent 65355 403eabd73c9a
child 65358 e345e9420109
--- a/src/Pure/PIDE/resources.scala	Mon Apr 03 12:49:13 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 13:39:13 2017 +0200
@@ -77,9 +77,6 @@
     }
     else Nil
 
-  private def dummy_name(theory: String): Document.Node.Name =
-    Document.Node.Name(theory + ".thy", "", theory)
-
   def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
   {
     val no_qualifier = "" // FIXME
@@ -88,12 +85,12 @@
     (base.known_theories.get(thy1) orElse
      base.known_theories.get(thy2) orElse
      base.known_theories.get(Long_Name.base_name(thy1))) match {
-      case Some(name) if base.loaded_theory(name) => dummy_name(name.theory)
+      case Some(name) if base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
       case Some(name) => name
       case None =>
         val path = Path.explode(s)
         val theory = path.base.implode
-        if (Long_Name.is_qualified(theory)) dummy_name(theory)
+        if (Long_Name.is_qualified(theory)) Document.Node.Name.theory(theory)
         else {
           val node = append(master.master_dir, thy_path(path))
           val master_dir = append(master.master_dir, path.dir)