src/Tools/jEdit/src/jedit_resources.scala
changeset 65532 febfd9f78bd4
parent 65524 0910f1733909
child 66195 bb886f13623a
equal deleted inserted replaced
65531:24544e3f183d 65532:febfd9f78bd4
    30 
    30 
    31   def node_name(path: String): Document.Node.Name =
    31   def node_name(path: String): Document.Node.Name =
    32     known_file(path) getOrElse {
    32     known_file(path) getOrElse {
    33       val vfs = VFSManager.getVFSForPath(path)
    33       val vfs = VFSManager.getVFSForPath(path)
    34       val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
    34       val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
    35       theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
    35       theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
    36         case (true, theory) => Document.Node.Name.loaded_theory(theory)
    36         case (true, theory) => Document.Node.Name.loaded_theory(theory)
    37         case (false, theory) =>
    37         case (false, theory) =>
    38           val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    38           val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    39           Document.Node.Name(node, master_dir, theory)
    39           Document.Node.Name(node, master_dir, theory)
    40       }
    40       }