# HG changeset patch
# User wenzelm
# Date 1283101469 -7200
# Node ID 9483bb678d968ede1348401ce316cfdafbd5494b
# Parent  57043221eb439670abb2e22386d597461ba91f32
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;

diff -r 57043221eb43 -r 9483bb678d96 src/Pure/Concurrent/future.scala
--- a/src/Pure/Concurrent/future.scala	Sun Aug 29 18:55:48 2010 +0200
+++ b/src/Pure/Concurrent/future.scala	Sun Aug 29 19:04:29 2010 +0200
@@ -28,6 +28,7 @@
 {
   def peek: Option[Exn.Result[A]]
   def is_finished: Boolean = peek.isDefined
+  def get_finished: A = { require(is_finished); Exn.release(peek.get) }
   def join: A
   def map[B](f: A => B): Future[B] = Future.fork { f(join) }
 
diff -r 57043221eb43 -r 9483bb678d96 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Aug 29 18:55:48 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Aug 29 19:04:29 2010 +0200
@@ -163,6 +163,7 @@
       private val promise = Future.promise[Map[Command, Exec_ID]]
       def is_finished: Boolean = promise.is_finished
       def join: Map[Command, Exec_ID] = promise.join
+      def get_finished: Map[Command, Exec_ID] = promise.get_finished
       def assign(command_execs: List[(Command, Exec_ID)])
       {
         promise.fulfill(tmp_assignment ++ command_execs)
@@ -253,7 +254,7 @@
     def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
     {
       val found_stable = history.undo_list.find(change =>
-        change.is_finished && is_assigned(change.current.join))
+        change.is_finished && is_assigned(change.current.get_finished))
       require(found_stable.isDefined)
       val stable = found_stable.get
       val latest = history.undo_list.head
@@ -265,14 +266,14 @@
 
       new Snapshot
       {
-        val version = stable.current.join
+        val version = stable.current.get_finished
         val node = version.nodes(name)
         val is_outdated = !(pending_edits.isEmpty && latest == stable)
 
         def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
 
         def state(command: Command): Command.State =
-          try { the_exec_state(the_assignment(version).join.getOrElse(command, fail)) }
+          try { the_exec_state(the_assignment(version).get_finished.getOrElse(command, fail)) }
           catch { case _: State.Fail => command.empty_state }
 
         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
diff -r 57043221eb43 -r 9483bb678d96 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sun Aug 29 18:55:48 2010 +0200
+++ b/src/Pure/System/session.scala	Sun Aug 29 19:04:29 2010 +0200
@@ -126,10 +126,10 @@
     def handle_change(change: Document.Change)
     //{{{
     {
-      val previous = change.previous.join
-      val (node_edits, current) = change.result.join
+      val previous = change.previous.get_finished
+      val (node_edits, current) = change.result.get_finished
 
-      var former_assignment = global_state.peek().the_assignment(previous).join
+      var former_assignment = global_state.peek().the_assignment(previous).get_finished
       for {
         (name, Some(cmd_edits)) <- node_edits
         (prev, None) <- cmd_edits
@@ -250,7 +250,7 @@
           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; result.map(_ => this_actor ! change)
+          val this_actor = self; change.current.map(_ => this_actor ! change)
           reply(())
 
         case change: Document.Change if prover != null =>
@@ -276,8 +276,6 @@
             finished = true
           }
 
-        case TIMEOUT =>  // FIXME clarify!
-
         case bad if prover != null =>
           System.err.println("session_actor: ignoring bad message " + bad)
       }