src/Tools/jEdit/src/jedit_resources.scala
changeset 65469 78ace4a14975
parent 65452 9e9750a7932c
child 65471 05e5bffcf1d8
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 17:48:19 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 19:56:47 2017 +0200
     1.3 @@ -25,14 +25,6 @@
     1.4  {
     1.5    /* document node name */
     1.6  
     1.7 -  def node_name(buffer: Buffer): Document.Node.Name =
     1.8 -  {
     1.9 -    val node = JEdit_Lib.buffer_name(buffer)
    1.10 -    val theory = Thy_Header.theory_name(node)
    1.11 -    val master_dir = if (theory == "") "" else buffer.getDirectory
    1.12 -    Document.Node.Name(node, master_dir, theory)
    1.13 -  }
    1.14 -
    1.15    def node_name(path: String): Document.Node.Name =
    1.16    {
    1.17      val vfs = VFSManager.getVFSForPath(path)
    1.18 @@ -42,11 +34,8 @@
    1.19      Document.Node.Name(node, master_dir, theory)
    1.20    }
    1.21  
    1.22 -  def node_name_file(name: Document.Node.Name): Option[JFile] =
    1.23 -  {
    1.24 -    val vfs = VFSManager.getVFSForPath(name.node)
    1.25 -    if (vfs.isInstanceOf[FileVFS]) Some(new JFile(name.node)) else None
    1.26 -  }
    1.27 +  def node_name(buffer: Buffer): Document.Node.Name =
    1.28 +    node_name(JEdit_Lib.buffer_name(buffer))
    1.29  
    1.30    def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
    1.31    {