src/Tools/jEdit/src/jedit_resources.scala
changeset 65501 b42743f5b595
parent 65476 a72ae9eb4462
child 65524 0910f1733909
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 17 21:26:23 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 17 21:48:53 2017 +0200
     1.3 @@ -25,17 +25,20 @@
     1.4  {
     1.5    /* document node name */
     1.6  
     1.7 +  def known_file(path: String): Option[Document.Node.Name] =
     1.8 +    JEdit_Lib.check_file(path).flatMap(session_base.known_file(_))
     1.9 +
    1.10    def node_name(path: String): Document.Node.Name =
    1.11 -  {
    1.12 -    val vfs = VFSManager.getVFSForPath(path)
    1.13 -    val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
    1.14 -    theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
    1.15 -      case (true, theory) => Document.Node.Name.loaded_theory(theory)
    1.16 -      case (false, theory) =>
    1.17 -        val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    1.18 -        Document.Node.Name(node, master_dir, theory)
    1.19 +    known_file(path) getOrElse {
    1.20 +      val vfs = VFSManager.getVFSForPath(path)
    1.21 +      val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
    1.22 +      theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
    1.23 +        case (true, theory) => Document.Node.Name.loaded_theory(theory)
    1.24 +        case (false, theory) =>
    1.25 +          val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    1.26 +          Document.Node.Name(node, master_dir, theory)
    1.27 +      }
    1.28      }
    1.29 -  }
    1.30  
    1.31    def node_name(buffer: Buffer): Document.Node.Name =
    1.32      node_name(JEdit_Lib.buffer_name(buffer))