src/Tools/jEdit/src/jedit_lib.scala

 package isabelle.jedit
 
 
 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}
 
 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}
 import org.gjt.sp.jedit.syntax.TokenMarker
 

 
     geometry
   }
 
 
+  /* 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 =
     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
 

       val name = mode.getName
       if (name == null) "" else name
     }
   }
 
-  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
-
   def buffer_line_manager(buffer: JEditBuffer): LineManager =
     Untyped.get[LineManager](buffer, "lineMgr")
+
+  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
+
+  def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer))
 
 
   /* main jEdit components */
 
   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator