tuned;
authorwenzelm
Fri, 12 Jul 2013 12:17:03 +0200
changeset 52608 f03c6a4d5870
parent 52607 33a133d50616
child 52609 c8f8c29193de
tuned;
src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Fri Jul 12 12:04:16 2013 +0200
+++ b/src/Pure/PIDE/execution.ML	Fri Jul 12 12:17:03 2013 +0200
@@ -2,7 +2,7 @@
     Author:     Makarius
 
 Global management of execution.  Unique running execution serves as
-barrier for further exploration of exec particles.
+barrier for further exploration of exec fragments.
 *)
 
 signature EXECUTION =
@@ -55,9 +55,8 @@
 fun finished exec_id =
   Synchronized.change state
     (apsnd (fn execs =>
-      Inttab.delete exec_id execs
-        handle Inttab.UNDEF bad =>
-          error ("Attempt to finish unknown execution: " ^ Document_ID.print bad)));
+      Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
+        error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
 
 fun peek exec_id =
   Inttab.lookup (snd (Synchronized.value state)) exec_id;