Future.promise: explicit abort operation (like uninterruptible future job);
explicit cancel_scala message -- still unused;

--- a/src/Pure/Concurrent/future.ML	Fri Aug 19 13:55:32 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Fri Aug 19 14:01:20 2011 +0200
@@ -62,8 +62,8 @@
   val value: 'a -> 'a future
   val map: ('a -> 'b) -> 'a future -> 'b future
   val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
-  val promise_group: Task_Queue.group -> 'a future
-  val promise: unit -> 'a future
+  val promise_group: Task_Queue.group -> (unit -> unit) -> 'a future
+  val promise: (unit -> unit) -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
   val fulfill: 'a future -> 'a -> unit
   val shutdown: unit -> unit
@@ -561,19 +561,23 @@
 
 (* promised futures -- fulfilled by external means *)
 
-fun promise_group group : 'a future =
+fun promise_group group abort : 'a future =
   let
     val result = Single_Assignment.var "promise" : 'a result;
-    fun abort () = assign_result group result Exn.interrupt_exn
+    fun assign () = assign_result group result Exn.interrupt_exn
       handle Fail _ => true
         | exn =>
-            if Exn.is_interrupt exn then raise Fail "Concurrent attempt to fulfill promise"
+            if Exn.is_interrupt exn
+            then raise Fail "Concurrent attempt to fulfill promise"
             else reraise exn;
+    fun job () =
+      Multithreading.with_attributes Multithreading.no_interrupts
+        (fn _ => assign () before abort ());
     val task = SYNCHRONIZED "enqueue_passive" (fn () =>
-      Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
+      Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job));
   in Future {promised = true, task = task, result = result} end;
 
-fun promise () = promise_group (worker_subgroup ());
+fun promise abort = promise_group (worker_subgroup ()) abort;
 
 fun fulfill_result (Future {promised, task, result}) res =
   if not promised then raise Fail "Not a promised future"

--- a/src/Pure/Concurrent/lazy.ML	Fri Aug 19 13:55:32 2011 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Fri Aug 19 14:01:20 2011 +0200
@@ -57,7 +57,7 @@
           val (expr, x) =
             Synchronized.change_result var
               (fn Expr e =>
-                    let val x = Future.promise ()
+                    let val x = Future.promise I
                     in ((SOME e, x), Result x) end
                 | Result x => ((NONE, x), Result x));
         in

--- a/src/Pure/General/markup.ML	Fri Aug 19 13:55:32 2011 +0200
+++ b/src/Pure/General/markup.ML	Fri Aug 19 14:01:20 2011 +0200
@@ -119,6 +119,7 @@
   val badN: string val bad: T
   val functionN: string
   val invoke_scala: string -> string -> Properties.T
+  val cancel_scala: string -> Properties.T
   val no_output: Output.output * Output.output
   val default_output: T -> Output.output * Output.output
   val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -377,6 +378,7 @@
 val functionN = "function"
 
 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
+fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
 
 

--- a/src/Pure/General/markup.scala	Fri Aug 19 13:55:32 2011 +0200
+++ b/src/Pure/General/markup.scala	Fri Aug 19 14:01:20 2011 +0200
@@ -283,6 +283,16 @@
       }
   }
 
+  val CANCEL_SCALA = "cancel_scala"
+  object Cancel_Scala
+  {
+    def unapply(props: Properties.T): Option[String] =
+      props match {
+        case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
+        case _ => None
+      }
+  }
+
 
   /* system data */
 

--- a/src/Pure/System/invoke_scala.ML	Fri Aug 19 13:55:32 2011 +0200
+++ b/src/Pure/System/invoke_scala.ML	Fri Aug 19 14:01:20 2011 +0200
@@ -33,7 +33,8 @@
 fun promise_method name arg =
   let
     val id = new_id ();
-    val promise = Future.promise () : string future;
+    fun abort () = Output.raw_message (Markup.cancel_scala id) "";
+    val promise = Future.promise abort : string future;
     val _ = Synchronized.change promises (Symtab.update (id, promise));
     val _ = Output.raw_message (Markup.invoke_scala name id) arg;
   in promise end;

--- a/src/Pure/System/session.scala	Fri Aug 19 13:55:32 2011 +0200
+++ b/src/Pure/System/session.scala	Fri Aug 19 14:01:20 2011 +0200
@@ -275,6 +275,8 @@
             val (tag, res) = Invoke_Scala.method(name, arg)
             prover.get.invoke_scala(id, tag, res)
           }
+        case Markup.Cancel_Scala(id) =>
+          System.err.println("cancel_scala " + id)  // FIXME cancel JVM task
         case _ =>
           if (result.is_syslog) {
             reverse_syslog ::= result.message