src/Pure/System/session.scala
changeset 38849 2f198d107aef
parent 38848 9483bb678d96
child 38850 5c3e5c548f12
     1.1 --- a/src/Pure/System/session.scala	Sun Aug 29 19:04:29 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sun Aug 29 19:48:35 2010 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4  
     1.5    case object Global_Settings
     1.6    case object Perspective
     1.7 +  case object Assignment
     1.8    case class Commands_Changed(set: Set[Command])
     1.9  }
    1.10  
    1.11 @@ -44,6 +45,7 @@
    1.12    val raw_output = new Event_Bus[Isabelle_Process.Result]
    1.13    val commands_changed = new Event_Bus[Session.Commands_Changed]
    1.14    val perspective = new Event_Bus[Session.Perspective.type]
    1.15 +  val assignments = new Event_Bus[Session.Assignment.type]
    1.16  
    1.17  
    1.18    /* unique ids */
    1.19 @@ -187,7 +189,10 @@
    1.20            if (result.is_status) {
    1.21              result.body match {
    1.22                case List(Isar_Document.Assign(id, edits)) =>
    1.23 -                try { global_state.change(_.assign(id, edits)) }
    1.24 +                try {
    1.25 +                  global_state.change(_.assign(id, edits))
    1.26 +                  assignments.event(Session.Assignment)
    1.27 +                }
    1.28                  catch { case _: Document.State.Fail => bad_result(result) }
    1.29                case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    1.30                case List(Keyword.Keyword_Decl(name)) => syntax += name
    1.31 @@ -250,7 +255,12 @@
    1.32            val previous = global_state.peek().history.tip.current
    1.33            val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
    1.34            val change = global_state.change_yield(_.extend_history(previous, edits, result))
    1.35 -          val this_actor = self; change.current.map(_ => this_actor ! change)
    1.36 +
    1.37 +          val this_actor = self
    1.38 +          change.current.map(_ => {
    1.39 +            assignments.await { global_state.peek().is_assigned(previous.get_finished) }
    1.40 +            this_actor ! change })
    1.41 +
    1.42            reply(())
    1.43  
    1.44          case change: Document.Change if prover != null =>