src/Tools/jEdit/src/jedit_resources.scala
changeset 76845 81848d12aba3
parent 76843 3dfc89c8dd71
child 76858 39db5e268aaf
equal deleted inserted replaced
76844:ef1f7d56f7c8 76845:81848d12aba3
    33   def node_name(path: String): Document.Node.Name =
    33   def node_name(path: String): Document.Node.Name =
    34     JEdit_Lib.check_file(path).flatMap(find_theory) getOrElse {
    34     JEdit_Lib.check_file(path).flatMap(find_theory) getOrElse {
    35       val vfs = VFSManager.getVFSForPath(path)
    35       val vfs = VFSManager.getVFSForPath(path)
    36       val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
    36       val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
    37       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
    37       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
    38       if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
    38       if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
    39       else {
    39       else {
    40         val master_dir = vfs.getParentOfPath(path)
    40         val master_dir = vfs.getParentOfPath(path)
    41         Document.Node.Name(node, master_dir = master_dir, theory = theory)
    41         Document.Node.Name(node, master_dir = master_dir, theory = theory)
    42       }
    42       }
    43     }
    43     }