--- 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)