use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled;
authorwenzelm
Sun Aug 29 19:04:29 2010 +0200 (2010-08-29)
changeset 388489483bb678d96
parent 38847 57043221eb43
child 38849 2f198d107aef
use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled;
clarified session signalling;
src/Pure/Concurrent/future.scala
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/Concurrent/future.scala	Sun Aug 29 18:55:48 2010 +0200
     1.2 +++ b/src/Pure/Concurrent/future.scala	Sun Aug 29 19:04:29 2010 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4  {
     1.5    def peek: Option[Exn.Result[A]]
     1.6    def is_finished: Boolean = peek.isDefined
     1.7 +  def get_finished: A = { require(is_finished); Exn.release(peek.get) }
     1.8    def join: A
     1.9    def map[B](f: A => B): Future[B] = Future.fork { f(join) }
    1.10  
     2.1 --- a/src/Pure/PIDE/document.scala	Sun Aug 29 18:55:48 2010 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sun Aug 29 19:04:29 2010 +0200
     2.3 @@ -163,6 +163,7 @@
     2.4        private val promise = Future.promise[Map[Command, Exec_ID]]
     2.5        def is_finished: Boolean = promise.is_finished
     2.6        def join: Map[Command, Exec_ID] = promise.join
     2.7 +      def get_finished: Map[Command, Exec_ID] = promise.get_finished
     2.8        def assign(command_execs: List[(Command, Exec_ID)])
     2.9        {
    2.10          promise.fulfill(tmp_assignment ++ command_execs)
    2.11 @@ -253,7 +254,7 @@
    2.12      def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
    2.13      {
    2.14        val found_stable = history.undo_list.find(change =>
    2.15 -        change.is_finished && is_assigned(change.current.join))
    2.16 +        change.is_finished && is_assigned(change.current.get_finished))
    2.17        require(found_stable.isDefined)
    2.18        val stable = found_stable.get
    2.19        val latest = history.undo_list.head
    2.20 @@ -265,14 +266,14 @@
    2.21  
    2.22        new Snapshot
    2.23        {
    2.24 -        val version = stable.current.join
    2.25 +        val version = stable.current.get_finished
    2.26          val node = version.nodes(name)
    2.27          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    2.28  
    2.29          def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
    2.30  
    2.31          def state(command: Command): Command.State =
    2.32 -          try { the_exec_state(the_assignment(version).join.getOrElse(command, fail)) }
    2.33 +          try { the_exec_state(the_assignment(version).get_finished.getOrElse(command, fail)) }
    2.34            catch { case _: State.Fail => command.empty_state }
    2.35  
    2.36          def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
     3.1 --- a/src/Pure/System/session.scala	Sun Aug 29 18:55:48 2010 +0200
     3.2 +++ b/src/Pure/System/session.scala	Sun Aug 29 19:04:29 2010 +0200
     3.3 @@ -126,10 +126,10 @@
     3.4      def handle_change(change: Document.Change)
     3.5      //{{{
     3.6      {
     3.7 -      val previous = change.previous.join
     3.8 -      val (node_edits, current) = change.result.join
     3.9 +      val previous = change.previous.get_finished
    3.10 +      val (node_edits, current) = change.result.get_finished
    3.11  
    3.12 -      var former_assignment = global_state.peek().the_assignment(previous).join
    3.13 +      var former_assignment = global_state.peek().the_assignment(previous).get_finished
    3.14        for {
    3.15          (name, Some(cmd_edits)) <- node_edits
    3.16          (prev, None) <- cmd_edits
    3.17 @@ -250,7 +250,7 @@
    3.18            val previous = global_state.peek().history.tip.current
    3.19            val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
    3.20            val change = global_state.change_yield(_.extend_history(previous, edits, result))
    3.21 -          val this_actor = self; result.map(_ => this_actor ! change)
    3.22 +          val this_actor = self; change.current.map(_ => this_actor ! change)
    3.23            reply(())
    3.24  
    3.25          case change: Document.Change if prover != null =>
    3.26 @@ -276,8 +276,6 @@
    3.27              finished = true
    3.28            }
    3.29  
    3.30 -        case TIMEOUT =>  // FIXME clarify!
    3.31 -
    3.32          case bad if prover != null =>
    3.33            System.err.println("session_actor: ignoring bad message " + bad)
    3.34        }