1.1 --- a/src/Pure/System/session.scala	Sat Jul 02 21:24:19 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sat Jul 02 23:04:19 2011 +0200
     1.3 @@ -16,6 +16,14 @@
     1.4  
     1.5  object Session
     1.6  {
     1.7 +  /* abstract file store */
     1.8 +
     1.9 +  abstract class File_Store
    1.10 +  {
    1.11 +    def read(path: Path): String
    1.12 +  }
    1.13 +
    1.14 +
    1.15    /* events */
    1.16  
    1.17    case object Global_Settings
    1.18 @@ -32,7 +40,7 @@
    1.19  }
    1.20  
    1.21  
    1.22 -class Session(val system: Isabelle_System)
    1.23 +class Session(val system: Isabelle_System, val file_store: Session.File_Store)
    1.24  {
    1.25    /* real time parameters */  // FIXME properties or settings (!?)
    1.26  

     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Jul 02 21:24:19 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Jul 02 23:04:19 2011 +0200
     2.3 @@ -10,14 +10,14 @@
     2.4  import isabelle._
     2.5  
     2.6  import java.lang.System
     2.7 -import java.io.{FileInputStream, IOException}
     2.8 +import java.io.{File, FileInputStream, IOException}
     2.9  import java.awt.Font
    2.10  
    2.11  import scala.collection.mutable
    2.12  import scala.swing.ComboBox
    2.13  
    2.14  import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
    2.15 -  Buffer, EditPane, ServiceManager, View}
    2.16 +  Buffer, EditPane, MiscUtilities, ServiceManager, View}
    2.17  import org.gjt.sp.jedit.buffer.JEditBuffer
    2.18  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    2.19  import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
    2.20 @@ -314,7 +314,25 @@
    2.21  
    2.22  class Plugin extends EBPlugin
    2.23  {
    2.24 -  /* session management */
    2.25 +  /* editor file store */
    2.26 +
    2.27 +  private val file_store = new Session.File_Store
    2.28 +  {
    2.29 +    def read(path: Path): String =
    2.30 +    {
    2.31 +      val platform_path = Isabelle.system.platform_path(path)
    2.32 +      val canonical_path = MiscUtilities.resolveSymlinks(platform_path)
    2.33 +
    2.34 +      Isabelle.jedit_buffers().find(buffer =>
    2.35 +          MiscUtilities.resolveSymlinks(buffer.getPath) == canonical_path) match {
    2.36 +        case Some(buffer) => Isabelle.buffer_text(buffer)
    2.37 +        case None => Standard_System.read_file(new File(platform_path))
    2.38 +      }
    2.39 +    }
    2.40 +  }
    2.41 +
    2.42 +
    2.43 +  /* session manager */
    2.44  
    2.45    private val session_manager = actor {
    2.46      loop {
    2.47 @@ -389,7 +407,7 @@
    2.48      Isabelle.setup_tooltips()
    2.49      Isabelle.system = new Isabelle_System
    2.50      Isabelle.system.install_fonts()
    2.51 -    Isabelle.session = new Session(Isabelle.system)
    2.52 +    Isabelle.session = new Session(Isabelle.system, file_store)
    2.53      SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender(Isabelle.system.symbols))
    2.54      if (ModeProvider.instance.isInstanceOf[ModeProvider])
    2.55        ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)