# HG changeset patch
# User wenzelm
# Date 1309640659 -7200
# Node ID ac886d096c11b8dcb7e79b5faa9eed8e2881e869
# Parent  ea08ce1c314bdbd7dd8ff00ee896e0add64bd87d
some support for Session.File_Store;

diff -r ea08ce1c314b -r ac886d096c11 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Jul 02 21:24:19 2011 +0200
+++ b/src/Pure/System/session.scala	Sat Jul 02 23:04:19 2011 +0200
@@ -16,6 +16,14 @@
 
 object Session
 {
+  /* abstract file store */
+
+  abstract class File_Store
+  {
+    def read(path: Path): String
+  }
+
+
   /* events */
 
   case object Global_Settings
@@ -32,7 +40,7 @@
 }
 
 
-class Session(val system: Isabelle_System)
+class Session(val system: Isabelle_System, val file_store: Session.File_Store)
 {
   /* real time parameters */  // FIXME properties or settings (!?)
 
diff -r ea08ce1c314b -r ac886d096c11 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sat Jul 02 21:24:19 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Jul 02 23:04:19 2011 +0200
@@ -10,14 +10,14 @@
 import isabelle._
 
 import java.lang.System
-import java.io.{FileInputStream, IOException}
+import java.io.{File, FileInputStream, IOException}
 import java.awt.Font
 
 import scala.collection.mutable
 import scala.swing.ComboBox
 
 import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
-  Buffer, EditPane, ServiceManager, View}
+  Buffer, EditPane, MiscUtilities, ServiceManager, View}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
@@ -314,7 +314,25 @@
 
 class Plugin extends EBPlugin
 {
-  /* session management */
+  /* editor file store */
+
+  private val file_store = new Session.File_Store
+  {
+    def read(path: Path): String =
+    {
+      val platform_path = Isabelle.system.platform_path(path)
+      val canonical_path = MiscUtilities.resolveSymlinks(platform_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))
+      }
+    }
+  }
+
+
+  /* session manager */
 
   private val session_manager = actor {
     loop {
@@ -389,7 +407,7 @@
     Isabelle.setup_tooltips()
     Isabelle.system = new Isabelle_System
     Isabelle.system.install_fonts()
-    Isabelle.session = new Session(Isabelle.system)
+    Isabelle.session = new Session(Isabelle.system, file_store)
     SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender(Isabelle.system.symbols))
     if (ModeProvider.instance.isInstanceOf[ModeProvider])
       ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)