src/Pure/PIDE/resources.scala
changeset 65357 9a2c266f97c8
parent 65355 403eabd73c9a
child 65358 e345e9420109
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 03 12:49:13 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 13:39:13 2017 +0200
     1.3 @@ -77,9 +77,6 @@
     1.4      }
     1.5      else Nil
     1.6  
     1.7 -  private def dummy_name(theory: String): Document.Node.Name =
     1.8 -    Document.Node.Name(theory + ".thy", "", theory)
     1.9 -
    1.10    def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
    1.11    {
    1.12      val no_qualifier = "" // FIXME
    1.13 @@ -88,12 +85,12 @@
    1.14      (base.known_theories.get(thy1) orElse
    1.15       base.known_theories.get(thy2) orElse
    1.16       base.known_theories.get(Long_Name.base_name(thy1))) match {
    1.17 -      case Some(name) if base.loaded_theory(name) => dummy_name(name.theory)
    1.18 +      case Some(name) if base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
    1.19        case Some(name) => name
    1.20        case None =>
    1.21          val path = Path.explode(s)
    1.22          val theory = path.base.implode
    1.23 -        if (Long_Name.is_qualified(theory)) dummy_name(theory)
    1.24 +        if (Long_Name.is_qualified(theory)) Document.Node.Name.theory(theory)
    1.25          else {
    1.26            val node = append(master.master_dir, thy_path(path))
    1.27            val master_dir = append(master.master_dir, path.dir)