diff -r 63d460db4919 -r 51f8895b9ad9 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Aug 29 16:28:51 2011 +0200
+++ b/src/Pure/System/session.scala	Mon Aug 29 16:38:56 2011 +0200
@@ -50,6 +50,7 @@
   val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
   val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
   val update_delay = Time.seconds(0.5)  // GUI layout updates
+  val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
 
 
   /* pervasive event buses */
@@ -186,6 +187,7 @@
 
   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,
@@ -371,6 +373,8 @@
         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,
@@ -413,6 +417,11 @@
 
   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)