# HG changeset patch # User wenzelm # Date 1492019807 -7200 # Node ID 78ace4a1497560841691f670fd762975c8b01537 # Parent c41791ad75c39b61c95a08927fcba04539e2ce7b more explicit jEdit file operations; less redundant JEdit_Resources.node_name(); diff -r c41791ad75c3 -r 78ace4a14975 src/Tools/jEdit/src/document_model.scala --- 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) diff -r c41791ad75c3 -r 78ace4a14975 src/Tools/jEdit/src/jedit_lib.scala --- 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 */ diff -r c41791ad75c3 -r 78ace4a14975 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] = {