Execution.fork formally requires registered Execution.running;
Thy_Info.load_thy: more official exec_id registration (batch mode);
dummy exec Document_ID.none is always registered (TTY mode);
clarified exceptions for module Execution (NB: fork is used in user space, unlike protocol operations of Command and Document);

--- a/src/Pure/PIDE/command.ML	Tue Sep 03 01:12:40 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Sep 03 11:29:01 2013 +0200
@@ -57,7 +57,7 @@
       (case expr of
         Expr (exec_id, body) =>
           uninterruptible (fn restore_attributes => fn () =>
-            if Execution.running execution_id exec_id then
+            if Execution.running execution_id exec_id [Future.the_worker_group ()] then
               let
                 val res =
                   (body

--- a/src/Pure/PIDE/execution.ML	Tue Sep 03 01:12:40 2013 +0200
+++ b/src/Pure/PIDE/execution.ML	Tue Sep 03 11:29:01 2013 +0200
@@ -11,7 +11,7 @@
   val discontinue: unit -> unit
   val is_running: Document_ID.execution -> bool
   val is_running_exec: Document_ID.exec -> bool
-  val running: Document_ID.execution -> Document_ID.exec -> bool
+  val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
   val peek: Document_ID.exec -> Future.group list
   val cancel: Document_ID.exec -> unit
   val terminate: Document_ID.exec -> unit
@@ -33,7 +33,7 @@
 fun make_state (execution, execs) = State {execution = execution, execs = execs};
 fun map_state f (State {execution, execs}) = make_state (f (execution, execs));
 
-val init_state = make_state (Document_ID.none, Inttab.empty);
+val init_state = make_state (Document_ID.none, Inttab.make [(Document_ID.none, [])]);
 val state = Synchronized.var "Execution.state" init_state;
 
 fun get_state () = let val State args = Synchronized.value state in args end;
@@ -58,18 +58,18 @@
 fun is_running_exec exec_id =
   Inttab.defined (#execs (get_state ())) exec_id;
 
-fun running execution_id exec_id =
-  Synchronized.guarded_access state
+fun running execution_id exec_id groups =
+  Synchronized.change_result state
     (fn State {execution = execution_id', execs} =>
       let
         val continue = execution_id = execution_id';
         val execs' =
           if continue then
-            Inttab.update_new (exec_id, [Future.the_worker_group ()]) execs
+            Inttab.update_new (exec_id, groups) execs
               handle Inttab.DUP dup =>
-                error ("Execution already registered: " ^ Document_ID.print dup)
+                raise Fail ("Execution already registered: " ^ Document_ID.print dup)
           else execs;
-      in SOME (continue, make_state (execution_id', execs')) end);
+      in (continue, make_state (execution_id', execs')) end);
 
 fun peek exec_id =
   Inttab.lookup_list (#execs (get_state ())) exec_id;
@@ -89,7 +89,10 @@
     let
       val exec_id = the_default 0 (Position.parse_id pos);
       val group = Future.worker_subgroup ();
-      val _ = change_state (apsnd (Inttab.cons_list (exec_id, group)));
+      val _ = change_state (apsnd (fn execs =>
+        if Inttab.defined execs exec_id
+        then Inttab.cons_list (exec_id, group) execs
+        else raise Fail ("Cannot fork from unregistered execution: " ^ Document_ID.print exec_id)));
 
       val future =
         (singleton o Future.forks)
@@ -127,7 +130,7 @@
           if Inttab.defined execs' exec_id then ()
           else groups |> List.app (fn group =>
             if Task_Queue.is_canceled group then ()
-            else error ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
+            else raise Fail ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
     in execs' end);
 
 fun reset () =

--- a/src/Pure/Thy/thy_info.ML	Tue Sep 03 01:12:40 2013 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Sep 03 11:29:01 2013 +0200
@@ -165,18 +165,20 @@
 (* scheduling loader tasks *)
 
 datatype result =
-  Result of {theory: theory, id: serial, present: unit -> unit, commit: unit -> unit, weight: int};
+  Result of {theory: theory, exec_id: Document_ID.exec,
+    present: unit -> unit, commit: unit -> unit, weight: int};
 
-fun theory_result theory = Result {theory = theory, id = 0, present = I, commit = I, weight = 0};
+fun theory_result theory =
+  Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0};
 
 fun result_theory (Result {theory, ...}) = theory;
 fun result_present (Result {present, ...}) = present;
 fun result_commit (Result {commit, ...}) = commit;
 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
 
-fun join_theory (Result {theory, id, ...}) =
+fun join_theory (Result {theory, exec_id, ...}) =
   Exn.capture Thm.join_theory_proofs theory ::
-  map Exn.Exn (maps Task_Queue.group_status (Execution.peek id));
+  map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id));
 
 
 datatype task =
@@ -271,13 +273,19 @@
 
     val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
 
-    val id = serial ();
-    val text_pos = Position.put_id (Markup.print_int id) (Path.position thy_path);
+    val exec_id = Document_ID.make ();
+    val _ =
+      Execution.running Document_ID.none exec_id [] orelse
+        raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
+
+    val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
     val (theory, present, weight) =
       Thy_Load.load_thy last_timing update_time dir header text_pos text
         (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
     fun commit () = update_thy deps theory;
-  in Result {theory = theory, id = id, present = present, commit = commit, weight = weight} end;
+  in
+    Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
+  end;
 
 fun check_deps dir name =
   (case lookup_deps name of