src/Tools/jEdit/src/jedit_resources.scala
changeset 64858 e31cf6eaecb8
parent 64856 5e9bf964510a
child 65243 ba5ce07e06a7
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 21:51:39 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 22:54:48 2017 +0100
     1.3 @@ -47,6 +47,12 @@
     1.4      Document.Node.Name(node, master_dir, theory)
     1.5    }
     1.6  
     1.7 +  def node_name_file(name: Document.Node.Name): Option[JFile] =
     1.8 +  {
     1.9 +    val vfs = VFSManager.getVFSForPath(name.node)
    1.10 +    if (vfs.isInstanceOf[FileVFS]) Some(new JFile(name.node)) else None
    1.11 +  }
    1.12 +
    1.13    def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
    1.14    {
    1.15      val name = node_name(buffer)