tuned signature;
tuned comments;

--- a/src/Pure/PIDE/command.ML	Fri Jul 12 11:07:02 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Jul 12 11:28:03 2013 +0200
@@ -20,7 +20,7 @@
   type exec = eval * print list
   val no_exec: exec
   val exec_ids: exec option -> Document_ID.exec list
-  val exec: Execution.context -> exec -> unit
+  val exec: Document_ID.execution -> exec -> unit
 end;
 
 structure Command: COMMAND =

--- a/src/Pure/PIDE/document.ML	Fri Jul 12 11:07:02 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Jul 12 11:28:03 2013 +0200
@@ -18,8 +18,6 @@
   val init_state: state
   val define_command: Document_ID.command -> string -> string -> state -> state
   val remove_versions: Document_ID.version list -> state -> state
-  val discontinue_execution: state -> unit
-  val cancel_execution: state -> unit
   val start_execution: state -> unit
   val timing: bool Unsynchronized.ref
   val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
@@ -205,10 +203,10 @@
 
 (** main state -- document structure and execution process **)
 
-type execution = {version_id: Document_ID.version, context: Execution.context};
+type execution = {version_id: Document_ID.version, execution_id: Document_ID.execution};
 
-val no_execution = {version_id = Document_ID.none, context = Execution.no_context};
-fun make_execution version_id = {version_id = version_id, context = Execution.fresh_context ()};
+val no_execution = {version_id = Document_ID.none, execution_id = Document_ID.none};
+fun next_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
 
 abstype state = State of
  {versions: version Inttab.table,  (*version id -> document content*)
@@ -235,7 +233,7 @@
     let
       val versions' = Inttab.update_new (version_id, version) versions
         handle Inttab.DUP dup => err_dup "document version" dup;
-      val execution' = make_execution version_id;
+      val execution' = next_execution version_id;
     in (versions', commands, execution') end);
 
 fun the_version (State {versions, ...}) version_id =
@@ -296,17 +294,11 @@
 
 (* document execution *)
 
-fun discontinue_execution state =
-  Execution.drop_context (#context (execution_of state));
-
-fun cancel_execution state =
-  (Execution.drop_context (#context (execution_of state)); Execution.terminate_all ());
-
 fun start_execution state =
   let
-    val {version_id, context} = execution_of state;
+    val {version_id, execution_id} = execution_of state;
     val _ =
-      if Execution.is_running context then
+      if Execution.is_running execution_id then
         nodes_of (the_version state version_id) |> String_Graph.schedule
           (fn deps => fn (name, node) =>
             if not (visible_node node) andalso finished_theory node then
@@ -319,7 +311,8 @@
                   iterate_entries (fn (_, opt_exec) => fn () =>
                     (case opt_exec of
                       SOME exec =>
-                        if Execution.is_running context then SOME (Command.exec context exec)
+                        if Execution.is_running execution_id
+                        then SOME (Command.exec execution_id exec)
                         else NONE
                     | NONE => NONE)) node ()))
       else [];

--- a/src/Pure/PIDE/document_id.ML	Fri Jul 12 11:07:02 2013 +0200
+++ b/src/Pure/PIDE/document_id.ML	Fri Jul 12 11:28:03 2013 +0200
@@ -12,6 +12,7 @@
   type version = generic
   type command = generic
   type exec = generic
+  type execution = generic
   val none: generic
   val make: unit -> generic
   val parse: string -> generic
@@ -25,6 +26,7 @@
 type version = generic;
 type command = generic;
 type exec = generic;
+type execution = generic;
 
 val none = 0;
 val make = Counter.make ();

--- a/src/Pure/PIDE/execution.ML	Fri Jul 12 11:07:02 2013 +0200
+++ b/src/Pure/PIDE/execution.ML	Fri Jul 12 11:28:03 2013 +0200
@@ -1,17 +1,16 @@
 (*  Title:      Pure/PIDE/execution.ML
     Author:     Makarius
 
-Global management of command execution fragments.
+Global management of execution.  Unique running execution serves as
+barrier for further exploration of exec particles.
 *)
 
 signature EXECUTION =
 sig
-  type context
-  val no_context: context
-  val drop_context: context -> unit
-  val fresh_context: unit -> context
-  val is_running: context -> bool
-  val running: context -> Document_ID.exec -> bool
+  val start: unit -> Document_ID.execution
+  val discontinue: unit -> unit
+  val is_running: Document_ID.execution -> bool
+  val running: Document_ID.execution -> Document_ID.exec -> bool
   val finished: Document_ID.exec -> bool -> unit
   val is_stable: Document_ID.exec -> bool
   val peek_running: Document_ID.exec -> Future.group option
@@ -22,43 +21,37 @@
 structure Execution: EXECUTION =
 struct
 
-(* global state *)
-
-datatype context = Context of Document_ID.generic;
-val no_context = Context Document_ID.none;
-
 type status = Future.group option;  (*SOME group: running, NONE: canceled*)
-val state = Synchronized.var "Execution.state" (no_context, Inttab.empty: status Inttab.table);
+val state = Synchronized.var "Execution.state" (Document_ID.none, Inttab.empty: status Inttab.table);
 
 
-(* unique execution context *)
-
-fun drop_context context =
-  Synchronized.change state
-    (apfst (fn context' => if context = context' then no_context else context'));
+(* unique running execution *)
 
-fun fresh_context () =
+fun start () =
   let
-    val context = Context (Document_ID.make ());
-    val _ = Synchronized.change state (apfst (K context));
-  in context end;
+    val execution_id = Document_ID.make ();
+    val _ = Synchronized.change state (apfst (K execution_id));
+  in execution_id end;
 
-fun is_running context = context = fst (Synchronized.value state);
+fun discontinue () =
+  Synchronized.change state (apfst (K Document_ID.none));
+
+fun is_running execution_id = execution_id = fst (Synchronized.value state);
 
 
 (* registered execs *)
 
-fun running context exec_id =
+fun running execution_id exec_id =
   Synchronized.guarded_access state
-    (fn (current_context, execs) =>
+    (fn (execution_id', execs) =>
       let
-        val cont = context = current_context;
+        val continue = execution_id = execution_id';
         val execs' =
-          if cont then
+          if continue then
             Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
               handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
           else execs;
-      in SOME (cont, (current_context, execs')) end);
+      in SOME (continue, (execution_id', execs')) end);
 
 fun finished exec_id stable =
   Synchronized.change state
@@ -81,11 +74,11 @@
 
 fun purge_canceled () =
   Synchronized.guarded_access state
-    (fn (context, execs) =>
+    (fn (execution_id, execs) =>
       let
         val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
         val execs' = fold Inttab.delete canceled execs;
-      in SOME ((), (context, execs')) end);
+      in SOME ((), (execution_id, execs')) end);
 
 fun terminate_all () =
   let

--- a/src/Pure/PIDE/protocol.ML	Fri Jul 12 11:07:02 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Jul 12 11:28:03 2013 +0200
@@ -17,17 +17,17 @@
 
 val _ =
   Isabelle_Process.protocol_command "Document.discontinue_execution"
-    (fn [] => Document.discontinue_execution (Document.state ()));
+    (fn [] => Execution.discontinue ());
 
 val _ =
   Isabelle_Process.protocol_command "Document.cancel_execution"
-    (fn [] => Document.cancel_execution (Document.state ()));
+    (fn [] => (Execution.discontinue (); Execution.terminate_all ()));
 
 val _ =
   Isabelle_Process.protocol_command "Document.update"
     (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
       let
-        val _ = Document.discontinue_execution state;
+        val _ = Execution.discontinue ();
 
         val old_id = Document_ID.parse old_id_string;
         val new_id = Document_ID.parse new_id_string;