src/Pure/PIDE/resources.scala
changeset 66771 925d10a7a610
parent 66767 294c2e9a689e
child 66850 a91b6d80c911
     1.1 --- a/src/Pure/PIDE/resources.scala	Fri Oct 06 17:13:57 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Fri Oct 06 21:14:00 2017 +0200
     1.3 @@ -105,10 +105,14 @@
     1.4          session_base.known_theory(theory) match {
     1.5            case Some(node_name) => node_name
     1.6            case None =>
     1.7 -            val path = Path.explode(s)
     1.8 -            val node = append(dir, thy_path(path))
     1.9 -            val master_dir = append(dir, path.dir)
    1.10 -            Document.Node.Name(node, master_dir, theory)
    1.11 +            if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s))
    1.12 +              Document.Node.Name.loaded_theory(theory)
    1.13 +            else {
    1.14 +              val path = Path.explode(s)
    1.15 +              val node = append(dir, thy_path(path))
    1.16 +              val master_dir = append(dir, path.dir)
    1.17 +              Document.Node.Name(node, master_dir, theory)
    1.18 +            }
    1.19          }
    1.20      }
    1.21  
    1.22 @@ -136,9 +140,14 @@
    1.23  
    1.24    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.25    {
    1.26 -    val path = File.check_file(name.path)
    1.27 -    val reader = Scan.byte_reader(path.file)
    1.28 -    try { f(reader) } finally { reader.close }
    1.29 +    val path = name.path
    1.30 +    if (path.is_file) {
    1.31 +      val reader = Scan.byte_reader(path.file)
    1.32 +      try { f(reader) } finally { reader.close }
    1.33 +    }
    1.34 +    else if (name.node == name.theory)
    1.35 +      error("Cannot load theory " + quote(name.theory))
    1.36 +    else error ("Cannot load theory file " + path)
    1.37    }
    1.38  
    1.39    def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char],