src/Tools/jEdit/src/jedit_resources.scala

--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 17:48:19 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 19:56:47 2017 +0200
@@ -25,14 +25,6 @@
 {
   /* document node name */
 
-  def node_name(buffer: Buffer): Document.Node.Name =
-  {
-    val node = JEdit_Lib.buffer_name(buffer)
-    val theory = Thy_Header.theory_name(node)
-    val master_dir = if (theory == "") "" else buffer.getDirectory
-    Document.Node.Name(node, master_dir, theory)
-  }
-
   def node_name(path: String): Document.Node.Name =
   {
     val vfs = VFSManager.getVFSForPath(path)
@@ -42,11 +34,8 @@
     Document.Node.Name(node, master_dir, theory)
   }
 
-  def node_name_file(name: Document.Node.Name): Option[JFile] =
-  {
-    val vfs = VFSManager.getVFSForPath(name.node)
-    if (vfs.isInstanceOf[FileVFS]) Some(new JFile(name.node)) else None
-  }
+  def node_name(buffer: Buffer): Document.Node.Name =
+    node_name(JEdit_Lib.buffer_name(buffer))
 
   def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
   {