actual auto loading of required files;
eliminated File_Store in favour of Thy_Load;
tuned;

--- a/src/Pure/System/session.scala	Mon Aug 29 16:38:56 2011 +0200
+++ b/src/Pure/System/session.scala	Mon Aug 29 21:55:49 2011 +0200
@@ -16,15 +16,6 @@
 
 object Session
 {
-  /* file store */
-
-  abstract class File_Store
-  {
-    def append(master_dir: String, path: Path): String
-    def require(file: String): Unit
-  }
-
-
   /* events */
 
   //{{{
@@ -43,7 +34,7 @@
 }
 
 
-class Session(val file_store: Session.File_Store)
+class Session(thy_load: Thy_Load)
 {
   /* real time parameters */  // FIXME properties or settings (!?)
 
@@ -117,8 +108,6 @@
 
   @volatile var verbose: Boolean = false
 
-  @volatile private var loaded_theories: Set[String] = Set()
-
   @volatile private var syntax = new Outer_Syntax
   def current_syntax(): Outer_Syntax = syntax
 
@@ -143,23 +132,6 @@
 
   /* theory files */
 
-  val thy_load = new Thy_Load
-  {
-    override def is_loaded(name: String): Boolean =
-      loaded_theories.contains(name)
-
-    override def check_thy(dir: Path, name: String): (String, Thy_Header) =
-    {
-      val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
-      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
-      val text = Standard_System.read_file(file)
-      val header = Thy_Header.read(text)
-      (text, header)
-    }
-  }
-
-  val thy_info = new Thy_Info(thy_load)
-
   def header_edit(name: String, master_dir: String,
     header: Document.Node_Header): Document.Edit_Text =
   {
@@ -167,10 +139,10 @@
     {
       val thy_name = Thy_Header.base_name(s)
       if (thy_load.is_loaded(thy_name)) thy_name
-      else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
+      else thy_load.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
     }
     def norm_use(s: String): String =
-      file_store.append(master_dir, Path.explode(s))
+      thy_load.append(master_dir, Path.explode(s))
 
     val header1: Document.Node_Header =
       header match {
@@ -187,7 +159,6 @@
 
   private case class Start(timeout: Time, args: List[String])
   private case object Interrupt
-  private case class Check_Loaded_Files(ask: List[String] => Boolean)
   private case class Init_Node(name: String, master_dir: String,
     header: Document.Node_Header, perspective: Text.Perspective, text: String)
   private case class Edit_Node(name: String, master_dir: String,
@@ -337,7 +308,7 @@
                 catch { case _: Document.State.Fail => bad_result(result) }
               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
               case List(Keyword.Keyword_Decl(name)) => syntax += name
-              case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
+              case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
               case _ => bad_result(result)
             }
           }
@@ -373,8 +344,6 @@
         case Interrupt if prover.isDefined =>
           prover.get.interrupt
 
-        case Check_Loaded_Files(ask) => // FIXME
-
         case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
           // FIXME compare with existing node
           handle_edits(name, master_dir, header,
@@ -417,11 +386,6 @@
 
   def interrupt() { session_actor ! Interrupt }
 
-  def check_loaded_files(ask: List[String] => Boolean)
-  {
-    session_actor ! Check_Loaded_Files(ask)
-  }
-
   // FIXME simplify signature
   def init_node(name: String, master_dir: String,
     header: Document.Node_Header, perspective: Text.Perspective, text: String)

--- a/src/Pure/Thy/thy_info.scala	Mon Aug 29 16:38:56 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala	Mon Aug 29 21:55:49 2011 +0200
@@ -38,37 +38,38 @@
 
   /* dependencies */
 
-  type Deps = Map[String, Exn.Result[(String, Thy_Header)]]  // name -> (text, header)
+  type Deps = Map[String, Document.Node_Header]
 
-  private def require_thys(ignored: String => Boolean,
-      initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
-    (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
+  private def require_thys(initiators: List[String],
+      deps: Deps, thys: List[(String, String)]): Deps =
+    (deps /: thys)(require_thy(initiators, _, _))
 
-  private def require_thy(ignored: String => Boolean,
-      initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
+  private def require_thy(initiators: List[String], deps: Deps, thy: (String, String)): Deps =
   {
+    val (dir, str) = thy
     val path = Path.explode(str)
-    val name = path.base.implode
+    val thy_name = path.base.implode
+    val node_name = thy_load.append(dir, Thy_Header.thy_path(path))
 
-    if (deps.isDefinedAt(name) || ignored(name)) deps
+    if (deps.isDefinedAt(node_name) || thy_load.is_loaded(thy_name)) deps
     else {
-      val dir1 = dir + path.dir
+      val dir1 = thy_load.append(dir, path.dir)
       try {
-        if (initiators.contains(name)) error(cycle_msg(initiators))
-        val (text, header) =
-          try { thy_load.check_thy(dir1, name) }
+        if (initiators.contains(node_name)) error(cycle_msg(initiators))
+        val header =
+          try { thy_load.check_thy(node_name) }
           catch {
             case ERROR(msg) =>
-              cat_error(msg, "The error(s) above occurred while examining theory " +
-                quote(name) + required_by("\n", initiators))
+              cat_error(msg, "The error(s) above occurred while examining theory file " +
+                quote(node_name) + required_by("\n", initiators))
           }
-        require_thys(ignored, name :: initiators, dir1,
-          deps + (name -> Exn.Res(text, header)), header.imports)
+        val thys = header.imports.map(str => (dir1, str))
+        require_thys(node_name :: initiators, deps + (node_name -> Exn.Res(header)), thys)
       }
-      catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
+      catch { case e: Throwable => deps + (node_name -> Exn.Exn(e)) }
     }
   }
 
-  def dependencies(dir: Path, str: String): Deps =
-    require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)
+  def dependencies(thys: List[(String, String)]): Deps =
+    require_thys(Nil, Map.empty, thys)
 }

--- a/src/Pure/Thy/thy_load.scala	Mon Aug 29 16:38:56 2011 +0200
+++ b/src/Pure/Thy/thy_load.scala	Mon Aug 29 21:55:49 2011 +0200
@@ -8,8 +8,9 @@
 
 abstract class Thy_Load
 {
-  def is_loaded(name: String): Boolean
-
-  def check_thy(dir: Path, name: String): (String, Thy_Header)
+  def register_thy(thy_name: String)
+  def is_loaded(thy_name: String): Boolean
+  def append(master_dir: String, path: Path): String
+  def check_thy(node_name: String): Thy_Header
 }
 

--- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 29 16:38:56 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 29 21:55:49 2011 +0200
@@ -13,9 +13,11 @@
 import java.io.{File, FileInputStream, IOException}
 import java.awt.Font
 import javax.swing.JOptionPane
+import javax.swing.text.Segment
 
 import scala.collection.mutable
 import scala.swing.ComboBox
+import scala.util.Sorting
 
 import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
   Buffer, EditPane, MiscUtilities, ServiceManager, View}
@@ -187,12 +189,10 @@
   def buffer_text(buffer: JEditBuffer): String =
     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
 
+  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
+
   def buffer_path(buffer: Buffer): (String, String) =
-  {
-    val master_dir = buffer.getDirectory
-    val path = buffer.getSymlinkPath
-    (master_dir, path)
-  }
+    (buffer.getDirectory, buffer_name(buffer))
 
 
   /* document model and view */
@@ -347,10 +347,19 @@
 
 class Plugin extends EBPlugin
 {
-  /* editor file store */
+  /* theory files via editor document model */
+
+  val thy_load = new Thy_Load
+  {
+    private var loaded_theories: Set[String] = Set()
 
-  private val file_store = new Session.File_Store
-  {
+    def register_thy(thy_name: String)
+    {
+      synchronized { loaded_theories += thy_name }
+    }
+    def is_loaded(thy_name: String): Boolean =
+      synchronized { loaded_theories.contains(thy_name) }
+
     def append(master_dir: String, source_path: Path): String =
     {
       val path = source_path.expand
@@ -364,36 +373,58 @@
       }
     }
 
-    def require(canonical_name: String)
+    def check_thy(node_name: String): Thy_Header =
     {
-      Swing_Thread.later {
-        if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
-          jEdit.openFile(null: View, canonical_name)
+      Swing_Thread.now {
+        Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
+          case Some(buffer) =>
+            Isabelle.buffer_lock(buffer) {
+              val text = new Segment
+              buffer.getText(0, buffer.getLength, text)
+              Some(Thy_Header.read(text))
+            }
+          case None => None
+        }
+      } getOrElse {
+        val file = new File(node_name)  // FIXME load URL via jEdit VFS (!?)
+        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
+        Thy_Header.read(file)
       }
     }
   }
 
-
-  /* session manager */
+  val thy_info = new Thy_Info(thy_load)
 
   private lazy val delay_load =
-    Swing_Thread.delay_last(Isabelle.session.load_delay) {
-      def ask(files: List[String]): Boolean = Swing_Thread.now
+    Swing_Thread.delay_last(Isabelle.session.load_delay)
+    {
+      val buffers = Isabelle.jedit_buffers().toList
+      def loaded_buffer(name: String): Boolean =
+        buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
+
+      val thys =
+        for (buffer <- buffers; model <- Isabelle.document_model(buffer))
+          yield (model.master_dir, model.thy_name)
+      val files = thy_info.dependencies(thys).map(_._1).filterNot(loaded_buffer _)
+
+      val do_load = !files.isEmpty &&
         {
-          val file_list = new scala.swing.TextArea(files.mkString("\n"))
-          file_list.editable = false
-          val answer =
-            Library.confirm_dialog(jEdit.getActiveView(),
+          val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
+          val files_text = new scala.swing.TextArea(files_sorted.mkString("\n"))
+          files_text.editable = false
+          Library.confirm_dialog(jEdit.getActiveView(),
             "Auto loading of required files",
             JOptionPane.YES_NO_OPTION,
-            "The following files are required to resolve theory imports.",
-            "Reload now?",
-            file_list)
-          answer == 0
+            "The following files are required to resolve theory imports.  Reload now?",
+            files_text) == 0
         }
+      if (do_load)
+        for (file <- files if !loaded_buffer(file))
+          jEdit.openFile(null: View, file)
+    }
 
-      Isabelle.session.check_loaded_files(ask _)
-    }
+
+  /* session manager */
 
   private val session_manager = actor {
     loop {
@@ -471,7 +502,7 @@
     Isabelle.setup_tooltips()
     Isabelle_System.init()
     Isabelle_System.install_fonts()
-    Isabelle.session = new Session(file_store)
+    Isabelle.session = new Session(thy_load)
     SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
     if (ModeProvider.instance.isInstanceOf[ModeProvider])
       ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)