# HG changeset patch # User wenzelm # Date 1283104115 -7200 # Node ID 2f198d107aefa6fe3c6d565573851c992cbf5cd9 # Parent 9483bb678d968ede1348401ce316cfdafbd5494b session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations; diff -r 9483bb678d96 -r 2f198d107aef src/Pure/System/event_bus.scala --- a/src/Pure/System/event_bus.scala Sun Aug 29 19:04:29 2010 +0200 +++ b/src/Pure/System/event_bus.scala Sun Aug 29 19:48:35 2010 +0200 @@ -32,4 +32,29 @@ /* event invocation */ def event(x: Event) { synchronized { receivers.foreach(_ ! x) } } + + + /* await global condition -- triggered via bus events */ + + def await(cond: => Boolean) + { + case object Wait + val a = new Actor { + def act { + if (cond) react { case Wait => reply(()); exit(Wait) } + else { + loop { + react { + case trigger if trigger != Wait => + if (cond) { react { case Wait => reply(()); exit(Wait) } } + } + } + } + } + } + this += a + a.start + a !? Wait + this -= a + } } diff -r 9483bb678d96 -r 2f198d107aef src/Pure/System/session.scala --- a/src/Pure/System/session.scala Sun Aug 29 19:04:29 2010 +0200 +++ b/src/Pure/System/session.scala Sun Aug 29 19:48:35 2010 +0200 @@ -19,6 +19,7 @@ case object Global_Settings case object Perspective + case object Assignment case class Commands_Changed(set: Set[Command]) } @@ -44,6 +45,7 @@ val raw_output = new Event_Bus[Isabelle_Process.Result] val commands_changed = new Event_Bus[Session.Commands_Changed] val perspective = new Event_Bus[Session.Perspective.type] + val assignments = new Event_Bus[Session.Assignment.type] /* unique ids */ @@ -187,7 +189,10 @@ if (result.is_status) { result.body match { case List(Isar_Document.Assign(id, edits)) => - try { global_state.change(_.assign(id, edits)) } + try { + global_state.change(_.assign(id, edits)) + assignments.event(Session.Assignment) + } catch { case _: Document.State.Fail => bad_result(result) } case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) case List(Keyword.Keyword_Decl(name)) => syntax += name @@ -250,7 +255,12 @@ val previous = global_state.peek().history.tip.current val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) } val change = global_state.change_yield(_.extend_history(previous, edits, result)) - val this_actor = self; change.current.map(_ => this_actor ! change) + + val this_actor = self + change.current.map(_ => { + assignments.await { global_state.peek().is_assigned(previous.get_finished) } + this_actor ! change }) + reply(()) case change: Document.Change if prover != null =>