src/Tools/jEdit/src/plugin.scala
changeset 44163 32e0c150c010
parent 44160 8848867501fb
child 44185 05641edb5d30
--- a/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 20:32:25 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 22:10:49 2011 +0200
@@ -327,15 +327,20 @@
 
   private val file_store = new Session.File_Store
   {
-    def read(path: Path): String =
+    def append(master_dir: String, path: Path): String =
     {
-      val platform_path = Isabelle_System.platform_path(path)
-      val canonical_path = MiscUtilities.resolveSymlinks(platform_path)
+      val vfs = VFSManager.getVFSForPath(master_dir)
+      if (vfs.isInstanceOf[FileVFS])
+        MiscUtilities.resolveSymlinks(
+          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
+      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
+    }
 
-      Isabelle.jedit_buffers().find(buffer =>
-          MiscUtilities.resolveSymlinks(buffer.getPath) == canonical_path) match {
-        case Some(buffer) => Isabelle.buffer_text(buffer)
-        case None => Standard_System.read_file(new File(platform_path))
+    def require(canonical_name: String)
+    {
+      Swing_Thread.later {
+        if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
+          jEdit.openFile(null: View, canonical_name)
       }
     }
   }