tuned;
authorwenzelm
Fri Jul 12 12:17:03 2013 +0200 (2013-07-12 ago)
changeset 52608f03c6a4d5870
parent 52607 33a133d50616
child 52609 c8f8c29193de
tuned;
src/Pure/PIDE/execution.ML
     1.1 --- a/src/Pure/PIDE/execution.ML	Fri Jul 12 12:04:16 2013 +0200
     1.2 +++ b/src/Pure/PIDE/execution.ML	Fri Jul 12 12:17:03 2013 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Makarius
     1.5  
     1.6  Global management of execution.  Unique running execution serves as
     1.7 -barrier for further exploration of exec particles.
     1.8 +barrier for further exploration of exec fragments.
     1.9  *)
    1.10  
    1.11  signature EXECUTION =
    1.12 @@ -55,9 +55,8 @@
    1.13  fun finished exec_id =
    1.14    Synchronized.change state
    1.15      (apsnd (fn execs =>
    1.16 -      Inttab.delete exec_id execs
    1.17 -        handle Inttab.UNDEF bad =>
    1.18 -          error ("Attempt to finish unknown execution: " ^ Document_ID.print bad)));
    1.19 +      Inttab.delete exec_id execs handle Inttab.UNDEF bad =>
    1.20 +        error ("Attempt to finish unknown execution " ^ Document_ID.print bad)));
    1.21  
    1.22  fun peek exec_id =
    1.23    Inttab.lookup (snd (Synchronized.value state)) exec_id;