src/Pure/System/session.scala
changeset 37129 4c83696b340e
parent 37065 2a73253b5898
child 37132 10ef4da1c314
     1.1 --- a/src/Pure/System/session.scala	Wed May 26 18:19:36 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Thu May 27 00:47:15 2010 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    trait Entity
     1.5    {
     1.6      val id: Entity_ID
     1.7 -    def consume(session: Session, message: XML.Tree): Unit
     1.8 +    def consume(message: XML.Tree, forward: Command => Unit): Unit
     1.9    }
    1.10  }
    1.11  
    1.12 @@ -37,9 +37,7 @@
    1.13    val global_settings = new Event_Bus[Session.Global_Settings.type]
    1.14    val raw_results = new Event_Bus[Isabelle_Process.Result]
    1.15    val raw_output = new Event_Bus[Isabelle_Process.Result]
    1.16 -  val results = new Event_Bus[Command]
    1.17 -
    1.18 -  val command_change = new Event_Bus[Command]
    1.19 +  val commands_changed = new Event_Bus[Command_Set]
    1.20  
    1.21  
    1.22    /* unique ids */
    1.23 @@ -66,7 +64,7 @@
    1.24    private case object Stop
    1.25    private case class Begin_Document(path: String)
    1.26  
    1.27 -  private val session_actor = actor {
    1.28 +  private lazy val session_actor = actor {
    1.29  
    1.30      var prover: Isabelle_Process with Isar_Document = null
    1.31  
    1.32 @@ -118,7 +116,7 @@
    1.33            case None => None
    1.34            case Some(id) => lookup_entity(id)
    1.35          }
    1.36 -      if (target.isDefined) target.get.consume(this, result.message)
    1.37 +      if (target.isDefined) target.get.consume(result.message, indicate_command_change)
    1.38        else if (result.kind == Isabelle_Process.Kind.STATUS) {
    1.39          // global status message
    1.40          result.body match {
    1.41 @@ -239,6 +237,52 @@
    1.42    }
    1.43  
    1.44  
    1.45 +
    1.46 +  /** buffered command changes -- delay_first discipline **/
    1.47 +
    1.48 +  private lazy val command_change_buffer = actor {
    1.49 +    import scala.compat.Platform.currentTime
    1.50 +
    1.51 +    var changed: Set[Command] = Set()
    1.52 +    var flush_time: Option[Long] = None
    1.53 +
    1.54 +    def flush_timeout: Long =
    1.55 +      flush_time match {
    1.56 +        case None => 5000L
    1.57 +        case Some(time) => (time - currentTime) max 0
    1.58 +      }
    1.59 +
    1.60 +    def flush()
    1.61 +    {
    1.62 +      if (!changed.isEmpty) commands_changed.event(Command_Set(changed))
    1.63 +      changed = Set()
    1.64 +      flush_time = None
    1.65 +    }
    1.66 +
    1.67 +    def invoke()
    1.68 +    {
    1.69 +      val now = currentTime
    1.70 +      flush_time match {
    1.71 +        case None => flush_time = Some(now + 100)
    1.72 +        case Some(time) => if (now >= time) flush()
    1.73 +      }
    1.74 +    }
    1.75 +
    1.76 +    loop {
    1.77 +      reactWithin(flush_timeout) {
    1.78 +        case command: Command => changed += command; invoke()
    1.79 +        case TIMEOUT => flush()
    1.80 +        case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
    1.81 +      }
    1.82 +    }
    1.83 +  }
    1.84 +
    1.85 +  def indicate_command_change(command: Command)
    1.86 +  {
    1.87 +    command_change_buffer ! command
    1.88 +  }
    1.89 +
    1.90 +
    1.91    /* main methods */
    1.92  
    1.93    def start(timeout: Int, args: List[String]): Option[String] =