1.1 --- a/src/Pure/System/session.scala	Mon Aug 29 16:28:51 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Mon Aug 29 16:38:56 2011 +0200
     1.3 @@ -50,6 +50,7 @@
     1.4    val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
     1.5    val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
     1.6    val update_delay = Time.seconds(0.5)  // GUI layout updates
     1.7 +  val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
     1.8  
     1.9  
    1.10    /* pervasive event buses */
    1.11 @@ -186,6 +187,7 @@
    1.12  
    1.13    private case class Start(timeout: Time, args: List[String])
    1.14    private case object Interrupt
    1.15 +  private case class Check_Loaded_Files(ask: List[String] => Boolean)
    1.16    private case class Init_Node(name: String, master_dir: String,
    1.17      header: Document.Node_Header, perspective: Text.Perspective, text: String)
    1.18    private case class Edit_Node(name: String, master_dir: String,
    1.19 @@ -371,6 +373,8 @@
    1.20          case Interrupt if prover.isDefined =>
    1.21            prover.get.interrupt
    1.22  
    1.23 +        case Check_Loaded_Files(ask) => // FIXME
    1.24 +
    1.25          case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
    1.26            // FIXME compare with existing node
    1.27            handle_edits(name, master_dir, header,
    1.28 @@ -413,6 +417,11 @@
    1.29  
    1.30    def interrupt() { session_actor ! Interrupt }
    1.31  
    1.32 +  def check_loaded_files(ask: List[String] => Boolean)
    1.33 +  {
    1.34 +    session_actor ! Check_Loaded_Files(ask)
    1.35 +  }
    1.36 +
    1.37    // FIXME simplify signature
    1.38    def init_node(name: String, master_dir: String,
    1.39      header: Document.Node_Header, perspective: Text.Perspective, text: String)