more explicit jEdit file operations;
authorwenzelm
Wed Apr 12 19:56:47 2017 +0200 (2017-04-12 ago)
changeset 6546978ace4a14975
parent 65468 c41791ad75c3
child 65470 a0f49174dbeb
more explicit jEdit file operations;
less redundant JEdit_Resources.node_name();
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Apr 12 17:48:19 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Apr 12 19:56:47 2017 +0200
     1.3 @@ -310,7 +310,7 @@
     1.4      last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
     1.5      pending_edits: List[Text.Edit] = Nil): File_Model =
     1.6    {
     1.7 -    val file = PIDE.resources.node_name_file(node_name)
     1.8 +    val file = JEdit_Lib.check_file(node_name.node)
     1.9      file.foreach(PIDE.plugin.file_watcher.register_parent(_))
    1.10  
    1.11      val content = Document_Model.File_Content(text)
     2.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Wed Apr 12 17:48:19 2017 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Apr 12 19:56:47 2017 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4  
     2.5  import isabelle._
     2.6  
     2.7 +import java.io.{File => JFile}
     2.8  import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension}
     2.9  import java.awt.event.{InputEvent, KeyEvent, KeyListener}
    2.10  import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
    2.11 @@ -16,6 +17,7 @@
    2.12  import scala.util.parsing.input.CharSequenceReader
    2.13  
    2.14  import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
    2.15 +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
    2.16  import org.gjt.sp.jedit.gui.KeyEventWorkaround
    2.17  import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
    2.18  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
    2.19 @@ -93,6 +95,15 @@
    2.20    }
    2.21  
    2.22  
    2.23 +  /* files */
    2.24 +
    2.25 +  def is_file(name: String): Boolean =
    2.26 +    VFSManager.getVFSForPath(name).isInstanceOf[FileVFS]
    2.27 +
    2.28 +  def check_file(name: String): Option[JFile] =
    2.29 +    if (is_file(name)) Some(new JFile(name)) else None
    2.30 +
    2.31 +
    2.32    /* buffers */
    2.33  
    2.34    def buffer_text(buffer: JEditBuffer): String =
    2.35 @@ -111,10 +122,12 @@
    2.36      }
    2.37    }
    2.38  
    2.39 +  def buffer_line_manager(buffer: JEditBuffer): LineManager =
    2.40 +    Untyped.get[LineManager](buffer, "lineMgr")
    2.41 +
    2.42    def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    2.43  
    2.44 -  def buffer_line_manager(buffer: JEditBuffer): LineManager =
    2.45 -    Untyped.get[LineManager](buffer, "lineMgr")
    2.46 +  def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer))
    2.47  
    2.48  
    2.49    /* main jEdit components */
     3.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 17:48:19 2017 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 19:56:47 2017 +0200
     3.3 @@ -25,14 +25,6 @@
     3.4  {
     3.5    /* document node name */
     3.6  
     3.7 -  def node_name(buffer: Buffer): Document.Node.Name =
     3.8 -  {
     3.9 -    val node = JEdit_Lib.buffer_name(buffer)
    3.10 -    val theory = Thy_Header.theory_name(node)
    3.11 -    val master_dir = if (theory == "") "" else buffer.getDirectory
    3.12 -    Document.Node.Name(node, master_dir, theory)
    3.13 -  }
    3.14 -
    3.15    def node_name(path: String): Document.Node.Name =
    3.16    {
    3.17      val vfs = VFSManager.getVFSForPath(path)
    3.18 @@ -42,11 +34,8 @@
    3.19      Document.Node.Name(node, master_dir, theory)
    3.20    }
    3.21  
    3.22 -  def node_name_file(name: Document.Node.Name): Option[JFile] =
    3.23 -  {
    3.24 -    val vfs = VFSManager.getVFSForPath(name.node)
    3.25 -    if (vfs.isInstanceOf[FileVFS]) Some(new JFile(name.node)) else None
    3.26 -  }
    3.27 +  def node_name(buffer: Buffer): Document.Node.Name =
    3.28 +    node_name(JEdit_Lib.buffer_name(buffer))
    3.29  
    3.30    def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
    3.31    {