# HG changeset patch
# User wenzelm
# Date 1313790498 -7200
# Node ID d4decbd67703837bdfa14abbad62bf824c8a8f12
# Parent  d2a6f9af02f467aecd9dce5f71b7f63278d92765# Parent  7ee000ce539020379ddc85ce7455e6ea02544566
merged

diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Concurrent/future.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -31,6 +31,9 @@
     that lack regular result information, will pick up parallel
     exceptions from the cumulative group context (as Par_Exn).
 
+  * Future task groups may be canceled: present and future group
+    members will be interrupted eventually.
+
   * Promised "passive" futures are fulfilled by external means.  There
     is no associated evaluation task, but other futures can depend on
     them via regular join operations.
@@ -38,31 +41,35 @@
 
 signature FUTURE =
 sig
-  val worker_task: unit -> Task_Queue.task option
-  val worker_group: unit -> Task_Queue.group option
-  val worker_subgroup: unit -> Task_Queue.group
+  type task = Task_Queue.task
+  type group = Task_Queue.group
+  val new_group: group option -> group
+  val worker_task: unit -> task option
+  val worker_group: unit -> group option
+  val worker_subgroup: unit -> group
   type 'a future
-  val task_of: 'a future -> Task_Queue.task
+  val task_of: 'a future -> task
   val peek: 'a future -> 'a Exn.result option
   val is_finished: 'a future -> bool
   val get_finished: 'a future -> 'a
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
-  val cancel_group: Task_Queue.group -> unit
-  val cancel: 'a future -> unit
+  val cancel_group: group -> task list
+  val cancel: 'a future -> task list
   type fork_params =
-   {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
-    pri: int, interrupts: bool}
+    {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
   val forks: fork_params -> (unit -> 'a) list -> 'a future list
   val fork_pri: int -> (unit -> 'a) -> 'a future
   val fork: (unit -> 'a) -> 'a future
   val join_results: 'a future list -> 'a Exn.result list
   val join_result: 'a future -> 'a Exn.result
   val join: 'a future -> 'a
+  val join_tasks: task list -> unit
+  val value_result: 'a Exn.result -> 'a future
   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: 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
@@ -74,17 +81,22 @@
 
 (** future values **)
 
+type task = Task_Queue.task;
+type group = Task_Queue.group;
+val new_group = Task_Queue.new_group;
+
+
 (* identifiers *)
 
 local
-  val tag = Universal.tag () : Task_Queue.task option Universal.tag;
+  val tag = Universal.tag () : task option Universal.tag;
 in
   fun worker_task () = the_default NONE (Thread.getLocal tag);
   fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x;
 end;
 
 val worker_group = Option.map Task_Queue.group_of_task o worker_task;
-fun worker_subgroup () = Task_Queue.new_group (worker_group ());
+fun worker_subgroup () = new_group (worker_group ());
 
 fun worker_joining e =
   (case worker_task () of
@@ -103,7 +115,7 @@
 
 datatype 'a future = Future of
  {promised: bool,
-  task: Task_Queue.task,
+  task: task,
   result: 'a result};
 
 fun task_of (Future {task, ...}) = task;
@@ -157,7 +169,7 @@
 val queue = Unsynchronized.ref Task_Queue.empty;
 val next = Unsynchronized.ref 0;
 val scheduler = Unsynchronized.ref (NONE: Thread.thread option);
-val canceled = Unsynchronized.ref ([]: Task_Queue.group list);
+val canceled = Unsynchronized.ref ([]: group list);
 val do_shutdown = Unsynchronized.ref false;
 val max_workers = Unsynchronized.ref 0;
 val max_active = Unsynchronized.ref 0;
@@ -172,15 +184,6 @@
 
 (* cancellation primitives *)
 
-fun interruptible_task f x =
-  if Multithreading.available then
-    Multithreading.with_attributes
-      (if is_some (worker_task ())
-       then Multithreading.private_interrupts
-       else Multithreading.public_interrupts)
-      (fn _ => f x)
-  else interruptible f x;
-
 fun cancel_now group = (*requires SYNCHRONIZED*)
   Task_Queue.cancel (! queue) group;
 
@@ -189,6 +192,17 @@
   broadcast scheduler_event);
 
 
+fun interruptible_task f x =
+  (if Multithreading.available then
+    Multithreading.with_attributes
+      (if is_some (worker_task ())
+       then Multithreading.private_interrupts
+       else Multithreading.public_interrupts)
+      (fn _ => f x)
+   else interruptible f x)
+  before Multithreading.interrupted ();
+
+
 (* worker threads *)
 
 fun worker_exec (task, jobs) =
@@ -208,10 +222,10 @@
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
         val maximal = Unsynchronized.change_result queue (Task_Queue.finish task);
-        val _ = Exn.capture Multithreading.interrupted ();
+        val test = Exn.capture Multithreading.interrupted ();
         val _ =
-          if ok then ()
-          else if cancel_now group then ()
+          if ok andalso not (Exn.is_interrupt_exn test) then ()
+          else if null (cancel_now group) then ()
           else cancel_later group;
         val _ = broadcast work_finished;
         val _ = if maximal then () else signal work_available;
@@ -244,7 +258,7 @@
 fun worker_loop name =
   (case SYNCHRONIZED name (fn () => worker_next ()) of
     NONE => ()
-  | SOME work => (Exn.capture Multithreading.interrupted (); worker_exec work; worker_loop name));
+  | SOME work => (worker_exec work; worker_loop name));
 
 fun worker_start name = (*requires SYNCHRONIZED*)
   Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
@@ -345,7 +359,7 @@
       else
        (Multithreading.tracing 1 (fn () =>
           string_of_int (length (! canceled)) ^ " canceled groups");
-        Unsynchronized.change canceled (filter_out cancel_now);
+        Unsynchronized.change canceled (filter_out (null o cancel_now));
         broadcast_work ());
 
 
@@ -388,12 +402,15 @@
 
 (** futures **)
 
-(* cancellation *)
+(* cancel *)
 
-(*cancel: present and future group members will be interrupted eventually*)
-fun cancel_group group = SYNCHRONIZED "cancel" (fn () =>
- (if cancel_now group then () else cancel_later group;
-  signal work_available; scheduler_check ()));
+fun cancel_group group = SYNCHRONIZED "cancel_group" (fn () =>
+  let
+    val running = cancel_now group;
+    val _ =
+      if null running then ()
+      else (cancel_later group; signal work_available; scheduler_check ());
+  in running end);
 
 fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x));
 
@@ -430,8 +447,7 @@
               Multithreading.with_attributes
                 (if interrupts
                  then Multithreading.private_interrupts else Multithreading.no_interrupts)
-                (fn _ => Position.setmp_thread_data pos e ()) before
-              Multithreading.interrupted ()) ()
+                (fn _ => Position.setmp_thread_data pos e ())) ()
           else Exn.interrupt_exn;
       in assign_result group result res end;
   in (result, job) end;
@@ -440,8 +456,7 @@
 (* fork *)
 
 type fork_params =
- {name: string, group: Task_Queue.group option, deps: Task_Queue.task list,
-  pri: int, interrupts: bool};
+  {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
 
 fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
   if null es then []
@@ -469,7 +484,7 @@
     end;
 
 fun fork_pri pri e =
-  singleton (forks {name = "", group = NONE, deps = [], pri = pri, interrupts = true}) e;
+  (singleton o forks) {name = "fork", group = NONE, deps = [], pri = pri, interrupts = true} e;
 
 fun fork e = fork_pri 0 e;
 
@@ -521,21 +536,30 @@
 fun join_result x = singleton join_results x;
 fun join x = Exn.release (join_result x);
 
+fun join_tasks [] = ()
+  | join_tasks tasks =
+      (singleton o forks)
+        {name = "join_tasks", group = SOME (new_group NONE),
+          deps = tasks, pri = 0, interrupts = false} I
+      |> join;
+
 
 (* fast-path versions -- bypassing task queue *)
 
-fun value (x: 'a) =
+fun value_result (res: 'a Exn.result) =
   let
     val task = Task_Queue.dummy_task ();
     val group = Task_Queue.group_of_task task;
     val result = Single_Assignment.var "value" : 'a result;
-    val _ = assign_result group result (Exn.Res x);
+    val _ = assign_result group result res;
   in Future {promised = false, task = task, result = result} end;
 
+fun value x = value_result (Exn.Res x);
+
 fun map_future f x =
   let
     val task = task_of x;
-    val group = Task_Queue.new_group (SOME (Task_Queue.group_of_task task));
+    val group = new_group (SOME (Task_Queue.group_of_task task));
     val (result, job) = future_job group true (fn () => f (join x));
 
     val extended = SYNCHRONIZED "extend" (fn () =>
@@ -545,32 +569,36 @@
   in
     if extended then Future {promised = false, task = task, result = result}
     else
-      singleton
-        (forks {name = "Future.map", group = SOME group, deps = [task],
-          pri = Task_Queue.pri_of_task task, interrupts = true})
+      (singleton o forks)
+        {name = "map_future", group = SOME group, deps = [task],
+          pri = Task_Queue.pri_of_task task, interrupts = true}
         (fn () => f (join x))
   end;
 
 fun cond_forks args es =
   if Multithreading.enabled () then forks args es
-  else map (fn e => value (e ())) es;
+  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
 
 
 (* 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"
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Concurrent/lazy.ML	Fri Aug 19 23:48:18 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
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Concurrent/par_exn.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -22,7 +22,11 @@
 fun serial exn =
   (case get_exn_serial exn of
     SOME i => (i, exn)
-  | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
+  | NONE =>
+      let
+        val i = Library.serial ();
+        val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
+      in (i, exn') end);
 
 val the_serial = the o get_exn_serial;
 
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Concurrent/par_list.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -34,12 +34,13 @@
   then map (Exn.capture f) xs
   else
     let
-      val group = Task_Queue.new_group (Future.worker_group ());
+      val group = Future.new_group (Future.worker_group ());
       val futures =
         Future.forks {name = name, group = SOME group, deps = [], pri = 0, interrupts = true}
           (map (fn x => fn () => f x) xs);
       val results = Future.join_results futures
-        handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
+        handle exn =>
+          (if Exn.is_interrupt exn then ignore (Future.cancel_group group) else (); reraise exn);
     in results end;
 
 fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Concurrent/task_queue.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -31,7 +31,7 @@
   val known_task: queue -> task -> bool
   val all_passive: queue -> bool
   val status: queue -> {ready: int, pending: int, running: int, passive: int}
-  val cancel: queue -> group -> bool
+  val cancel: queue -> group -> task list
   val cancel_all: queue -> group list
   val finish: task -> queue -> bool * queue
   val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
@@ -248,10 +248,12 @@
   let
     val _ = cancel_group group Exn.Interrupt;
     val running =
-      Tasks.fold (#1 #> get_job jobs #> (fn Running t => insert Thread.equal t | _ => I))
+      Tasks.fold (fn (task, _) =>
+          (case get_job jobs task of Running thread => cons (task, thread) | _ => I))
         (get_tasks groups (group_id group)) [];
-    val _ = List.app Simple_Thread.interrupt_unsynchronized running;
-  in null running end;
+    val threads = fold (insert Thread.equal o #2) running [];
+    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
+  in map #1 running end;
 
 fun cancel_all (Queue {jobs, ...}) =
   let
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/General/markup.ML	Fri Aug 19 23:48:18 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)];
 
 
 
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/General/markup.scala	Fri Aug 19 23:48:18 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 */
 
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Isar/runtime.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -119,7 +119,7 @@
   else f x;
 
 fun controlled_execution f x =
-  ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
+  (f |> debugging |> Future.interruptible_task) x;
 
 fun toplevel_error output_exn f x = f x
   handle exn =>
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Isar/toplevel.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -419,6 +419,14 @@
 
 (* theory transitions *)
 
+val global_theory_group =
+  Sign.new_group #>
+  Global_Theory.begin_recent_proofs #> Theory.checkpoint;
+
+val local_theory_group =
+  Local_Theory.new_group #>
+  Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint);
+
 fun generic_theory f = transaction (fn _ =>
   (fn Theory (gthy, _) => Theory (f gthy, NONE)
     | _ => raise UNDEF));
@@ -426,8 +434,7 @@
 fun theory' f = transaction (fn int =>
   (fn Theory (Context.Theory thy, _) =>
       let val thy' = thy
-        |> Sign.new_group
-        |> Theory.checkpoint
+        |> global_theory_group
         |> f int
         |> Sign.reset_group;
       in Theory (Context.Theory thy', NONE) end
@@ -454,7 +461,7 @@
         let
           val finish = loc_finish loc gthy;
           val lthy' = loc_begin loc gthy
-            |> Local_Theory.new_group
+            |> local_theory_group
             |> f int
             |> Local_Theory.reset_group;
         in Theory (finish lthy', SOME lthy') end
@@ -506,13 +513,13 @@
 in
 
 fun local_theory_to_proof' loc f = begin_proof
-  (fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy)))
+  (fn int => fn gthy => f int (local_theory_group (loc_begin loc gthy)))
   (fn gthy => loc_finish loc gthy o Local_Theory.reset_group);
 
 fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
 
 fun theory_to_proof f = begin_proof
-  (K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
+  (K (fn Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF))
   (K (Context.Theory o Sign.reset_group o Proof_Context.theory_of));
 
 end;
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/PIDE/document.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -24,7 +24,7 @@
   type state
   val init_state: state
   val join_commands: state -> unit
-  val cancel_execution: state -> unit -> unit
+  val cancel_execution: state -> Future.task list
   val define_command: command_id -> string -> state -> state
   val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
   val execute: version_id -> state -> state
@@ -164,7 +164,7 @@
  {versions: version Inttab.table,  (*version_id -> document content*)
   commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
   execs: Toplevel.state lazy Inttab.table,  (*exec_id -> execution process*)
-  execution: unit future list}  (*global execution process*)
+  execution: Future.group}  (*global execution process*)
 with
 
 fun make_state (versions, commands, execs, execution) =
@@ -177,7 +177,7 @@
   make_state (Inttab.make [(no_id, empty_version)],
     Inttab.make [(no_id, Future.value Toplevel.empty)],
     Inttab.make [(no_id, empty_exec)],
-    []);
+    Future.new_group NONE);
 
 
 (* document versions *)
@@ -200,9 +200,10 @@
   map_state (fn (versions, commands, execs, execution) =>
     let
       val id_string = print_id id;
-      val tr = Future.fork_pri 2 (fn () =>
-        Position.setmp_thread_data (Position.id_only id_string)
-          (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
+      val tr =
+        Future.fork_pri 2 (fn () =>
+          Position.setmp_thread_data (Position.id_only id_string)
+            (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
       val commands' =
         Inttab.update_new (id, tr) commands
           handle Inttab.DUP dup => err_dup "command" dup;
@@ -233,9 +234,7 @@
 
 (* document execution *)
 
-fun cancel_execution (State {execution, ...}) =
-  (List.app Future.cancel execution;
-    fn () => ignore (Future.join_results execution));
+fun cancel_execution (State {execution, ...}) = Future.cancel_group execution;
 
 end;
 
@@ -253,13 +252,13 @@
   | NONE => ());
 
 fun async_state tr st =
-  ignore
-    (singleton
-      (Future.forks {name = "Document.async_state",
-        group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true})
-      (fn () =>
-        Toplevel.setmp_thread_position tr
-          (fn () => Toplevel.print_state false st) ()));
+  (singleton o Future.forks)
+    {name = "Document.async_state", group = SOME (Future.new_group NONE),
+      deps = [], pri = 0, interrupts = true}
+    (fn () =>
+      Toplevel.setmp_thread_position tr
+        (fn () => Toplevel.print_state false st) ())
+  |> ignore;
 
 fun run int tr st =
   (case Toplevel.transition int tr st of
@@ -355,9 +354,9 @@
                 fun get_command id =
                   (id, the_command state id |> Future.map (Toplevel.modify_init init));
               in
-                singleton
-                  (Future.forks {name = "Document.edit", group = NONE,
-                    deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false})
+                (singleton o Future.forks)
+                  {name = "Document.edit", group = NONE,
+                    deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
                   (fn () =>
                     let
                       val prev_exec =
@@ -393,17 +392,16 @@
       fun force_exec NONE = ()
         | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
 
-      val execution' =
+      val execution = Future.new_group NONE;
+      val _ =
         nodes_of version |> Graph.schedule
           (fn deps => fn (name, node) =>
-            singleton
-              (Future.forks
-                {name = "theory:" ^ name, group = NONE,
-                  deps = map (Future.task_of o #2) deps,
-                  pri = 1, interrupts = true})
+            (singleton o Future.forks)
+              {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
+                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
               (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
 
-    in (versions, commands, execs, execution') end);
+    in (versions, commands, execs, execution) end);
 
 
 
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/PIDE/isar_document.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -30,9 +30,9 @@
                   fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
             end;
 
-      val await_cancellation = Document.cancel_execution state;
+      val running = Document.cancel_execution state;
       val (updates, state') = Document.edit old_id new_id edits state;
-      val _ = await_cancellation ();
+      val _ = Future.join_tasks running;
       val _ = Document.join_commands state';
       val _ =
         Output.status (Markup.markup (Markup.assign new_id)
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/System/invoke_scala.ML
--- a/src/Pure/System/invoke_scala.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/System/invoke_scala.ML	Fri Aug 19 23:48:18 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;
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/System/session.scala	Fri Aug 19 23:48:18 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
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/Thy/thy_info.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -194,11 +194,9 @@
   Graph.schedule (fn deps => fn (name, task) =>
     (case task of
       Task (parents, body) =>
-        singleton
-          (Future.forks
-            {name = "theory:" ^ name, group = NONE,
-              deps = map (Future.task_of o #2) deps,
-              pri = 0, interrupts = true})
+        (singleton o Future.forks)
+          {name = "theory:" ^ name, group = NONE,
+            deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
           (fn () =>
             (case filter (not o can Future.join o #2) deps of
               [] => body (map (#1 o Future.join) (task_parents deps parents))
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/global_theory.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -10,6 +10,8 @@
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
   val hide_fact: bool -> string -> theory -> theory
+  val begin_recent_proofs: theory -> theory
+  val join_recent_proofs: theory -> unit
   val join_proofs: theory -> unit
   val get_fact: Context.generic -> theory -> Facts.ref -> thm list
   val get_thms: theory -> xstring -> thm list
@@ -49,10 +51,10 @@
 
 structure Data = Theory_Data
 (
-  type T = Facts.T * thm list;
-  val empty = (Facts.empty, []);
-  fun extend (facts, _) = (facts, []);
-  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
+  type T = Facts.T * (thm list * thm list);
+  val empty = (Facts.empty, ([], []));
+  fun extend (facts, _) = (facts, ([], []));
+  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), ([], []));
 );
 
 
@@ -68,10 +70,11 @@
 
 (* proofs *)
 
-fun register_proofs (thy, thms) = (Data.map (apsnd (append thms)) thy, thms);
+fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (append thms))) thy, thms);
 
-fun join_proofs thy = Thm.join_proofs (rev (#2 (Data.get thy)));
-
+val begin_recent_proofs = Data.map (apsnd (fn (_, thms) => ([], thms)));
+val join_recent_proofs = Thm.join_proofs o rev o #1 o #2 o Data.get;
+val join_proofs = Thm.join_proofs o rev o #2 o #2 o Data.get;
 
 
 (** retrieve theorems **)
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/goal.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -124,8 +124,8 @@
     let
       val _ = forked 1;
       val future =
-        singleton
-          (Future.forks {name = name, group = NONE, deps = [], pri = ~1, interrupts = false})
+        (singleton o Future.forks)
+          {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
           (fn () =>
             Exn.release
               (Exn.capture (Future.status o Future.interruptible_task) e before forked ~1));
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/proofterm.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -37,11 +37,11 @@
 
   type oracle = string * term
   type pthm = serial * (string * term * proof_body future)
+  val join_body: proof_body -> unit
   val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
-  val join_bodies: proof_body list -> unit
   val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
 
   val oracle_ord: oracle * oracle -> order
@@ -171,6 +171,10 @@
 type oracle = string * term;
 type pthm = serial * (string * term * proof_body future);
 
+fun join_thm (pthm: pthm) = ignore (Future.join (#3 (#2 pthm)));
+fun join_thms thms = (Future.join_results (map (#3 o #2) thms); List.app join_thm thms);
+fun join_body (PBody {thms, ...}) = join_thms thms;
+
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;
 
@@ -195,18 +199,15 @@
 fun fold_body_thms f =
   let
     fun app (PBody {thms, ...}) =
-     (Future.join_results (map (#3 o #2) thms);
-      thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
+      tap join_thms thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
         if Inttab.defined seen i then (x, seen)
         else
           let
             val body' = Future.join body;
             val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
-          in (f (name, prop, body') x', seen') end));
+          in (f (name, prop, body') x', seen') end);
   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
 
-fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
-
 fun status_of bodies =
   let
     fun status (PBody {oracles, thms, ...}) x =
@@ -242,14 +243,13 @@
 val all_oracles_of =
   let
     fun collect (PBody {oracles, thms, ...}) =
-     (Future.join_results (map (#3 o #2) thms);
-      thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
+      tap join_thms thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
         if Inttab.defined seen i then (x, seen)
         else
           let
             val body' = Future.join body;
             val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
-          in (merge_oracles oracles x', seen') end));
+          in (merge_oracles oracles x', seen') end);
   in fn body => #1 (collect body ([], Inttab.empty)) end;
 
 fun approximate_proof_body prf =
@@ -1396,16 +1396,17 @@
       | fill _ = NONE;
     val (rules, procs) = get_data thy;
     val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
+    val _ = join_thms thms;
   in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
 fun fulfill_proof_future _ [] postproc body =
       if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
       else Future.map postproc body
   | fulfill_proof_future thy promises postproc body =
-      singleton
-        (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
-            deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
-            interrupts = true})
+      (singleton o Future.forks)
+        {name = "Proofterm.fulfill_proof_future", group = NONE,
+          deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
+          interrupts = true}
         (fn () =>
           postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
 
@@ -1461,10 +1462,9 @@
       if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
       else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
       else
-        singleton
-          (Future.forks
-            {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1,
-              interrupts = true})
+        (singleton o Future.forks)
+          {name = "Proofterm.prepare_thm_proof", group = NONE,
+            deps = [], pri = ~1, interrupts = true}
           (make_body0 o full_proof0);
 
     fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
diff -r d2a6f9af02f4 -r d4decbd67703 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Pure/thm.ML	Fri Aug 19 23:48:18 2011 +0200
@@ -517,9 +517,9 @@
     (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
 and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
 
-val join_proofs = Proofterm.join_bodies o map fulfill_body;
+fun join_proofs thms = ignore (map fulfill_body thms);
 
-fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm);
+fun proof_body_of thm = (Proofterm.join_body (raw_body thm); fulfill_body thm);
 val proof_of = Proofterm.proof_of o proof_body_of;
 
 
diff -r d2a6f9af02f4 -r d4decbd67703 src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Aug 19 23:48:18 2011 +0200
@@ -21,7 +21,6 @@
   extends Dockable(view: View, position: String)
 {
   private val text_area = new TextArea
-  text_area.editable = false
   set_content(new ScrollPane(text_area))
 
 
diff -r d2a6f9af02f4 -r d4decbd67703 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Fri Aug 19 10:46:54 2011 -0700
+++ b/src/Tools/jEdit/src/session_dockable.scala	Fri Aug 19 23:48:18 2011 +0200
@@ -28,7 +28,6 @@
   readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
 
   private val syslog = new TextArea(Isabelle.session.syslog())
-  syslog.editable = false
 
   private val tabs = new TabbedPane {
     pages += new TabbedPane.Page("README", Component.wrap(readme))