# HG changeset patch # User wenzelm # Date 1373624223 -7200 # Node ID f03c6a4d587022e01407568349981b15da6a4279 # Parent 33a133d50616ed66fa24e4b7e2d28dd6e9d44171 tuned; diff -r 33a133d50616 -r f03c6a4d5870 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;