--- a/src/Tools/jEdit/src/document_model.scala Wed Apr 12 17:48:19 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Apr 12 19:56:47 2017 +0200
@@ -310,7 +310,7 @@
last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
pending_edits: List[Text.Edit] = Nil): File_Model =
{
- val file = PIDE.resources.node_name_file(node_name)
+ val file = JEdit_Lib.check_file(node_name.node)
file.foreach(PIDE.plugin.file_watcher.register_parent(_))
val content = Document_Model.File_Content(text)
--- a/src/Tools/jEdit/src/jedit_lib.scala Wed Apr 12 17:48:19 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Wed Apr 12 19:56:47 2017 +0200
@@ -9,6 +9,7 @@
import isabelle._
+import java.io.{File => JFile}
import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension}
import java.awt.event.{InputEvent, KeyEvent, KeyListener}
import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
@@ -16,6 +17,7 @@
import scala.util.parsing.input.CharSequenceReader
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
+import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
import org.gjt.sp.jedit.gui.KeyEventWorkaround
import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
@@ -93,6 +95,15 @@
}
+ /* files */
+
+ def is_file(name: String): Boolean =
+ VFSManager.getVFSForPath(name).isInstanceOf[FileVFS]
+
+ def check_file(name: String): Option[JFile] =
+ if (is_file(name)) Some(new JFile(name)) else None
+
+
/* buffers */
def buffer_text(buffer: JEditBuffer): String =
@@ -111,10 +122,12 @@
}
}
+ def buffer_line_manager(buffer: JEditBuffer): LineManager =
+ Untyped.get[LineManager](buffer, "lineMgr")
+
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
- def buffer_line_manager(buffer: JEditBuffer): LineManager =
- Untyped.get[LineManager](buffer, "lineMgr")
+ def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer))
/* main jEdit components */
--- 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] =
{