session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
authorwenzelm
Sun Aug 29 19:48:35 2010 +0200 (2010-08-29)
changeset 388492f198d107aef
parent 38848 9483bb678d96
child 38850 5c3e5c548f12
session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
src/Pure/System/event_bus.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/System/event_bus.scala	Sun Aug 29 19:04:29 2010 +0200
     1.2 +++ b/src/Pure/System/event_bus.scala	Sun Aug 29 19:48:35 2010 +0200
     1.3 @@ -32,4 +32,29 @@
     1.4    /* event invocation */
     1.5  
     1.6    def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
     1.7 +
     1.8 +
     1.9 +  /* await global condition -- triggered via bus events */
    1.10 +
    1.11 +  def await(cond: => Boolean)
    1.12 +  {
    1.13 +    case object Wait
    1.14 +    val a = new Actor {
    1.15 +      def act {
    1.16 +        if (cond) react { case Wait => reply(()); exit(Wait) }
    1.17 +        else {
    1.18 +          loop {
    1.19 +            react {
    1.20 +              case trigger if trigger != Wait =>
    1.21 +                if (cond) { react { case Wait => reply(()); exit(Wait) } }
    1.22 +            }
    1.23 +          }
    1.24 +        }
    1.25 +      }
    1.26 +    }
    1.27 +    this += a
    1.28 +    a.start
    1.29 +    a !? Wait
    1.30 +    this -= a
    1.31 +  }
    1.32  }
     2.1 --- a/src/Pure/System/session.scala	Sun Aug 29 19:04:29 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Sun Aug 29 19:48:35 2010 +0200
     2.3 @@ -19,6 +19,7 @@
     2.4  
     2.5    case object Global_Settings
     2.6    case object Perspective
     2.7 +  case object Assignment
     2.8    case class Commands_Changed(set: Set[Command])
     2.9  }
    2.10  
    2.11 @@ -44,6 +45,7 @@
    2.12    val raw_output = new Event_Bus[Isabelle_Process.Result]
    2.13    val commands_changed = new Event_Bus[Session.Commands_Changed]
    2.14    val perspective = new Event_Bus[Session.Perspective.type]
    2.15 +  val assignments = new Event_Bus[Session.Assignment.type]
    2.16  
    2.17  
    2.18    /* unique ids */
    2.19 @@ -187,7 +189,10 @@
    2.20            if (result.is_status) {
    2.21              result.body match {
    2.22                case List(Isar_Document.Assign(id, edits)) =>
    2.23 -                try { global_state.change(_.assign(id, edits)) }
    2.24 +                try {
    2.25 +                  global_state.change(_.assign(id, edits))
    2.26 +                  assignments.event(Session.Assignment)
    2.27 +                }
    2.28                  catch { case _: Document.State.Fail => bad_result(result) }
    2.29                case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    2.30                case List(Keyword.Keyword_Decl(name)) => syntax += name
    2.31 @@ -250,7 +255,12 @@
    2.32            val previous = global_state.peek().history.tip.current
    2.33            val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
    2.34            val change = global_state.change_yield(_.extend_history(previous, edits, result))
    2.35 -          val this_actor = self; change.current.map(_ => this_actor ! change)
    2.36 +
    2.37 +          val this_actor = self
    2.38 +          change.current.map(_ => {
    2.39 +            assignments.await { global_state.peek().is_assigned(previous.get_finished) }
    2.40 +            this_actor ! change })
    2.41 +
    2.42            reply(())
    2.43  
    2.44          case change: Document.Change if prover != null =>