tuned;
authorwenzelm
Fri Jul 17 21:00:41 2015 +0200 (2015-07-17)
changeset 607474ced3c6ad807
parent 60746 8cf877aca29a
child 60748 6d718fda8215
tuned;
src/Pure/Tools/simplifier_trace.ML
     1.1 --- a/src/Pure/Tools/simplifier_trace.ML	Fri Jul 17 17:17:39 2015 +0200
     1.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Fri Jul 17 21:00:41 2015 +0200
     1.3 @@ -395,17 +395,17 @@
     1.4  
     1.5  val _ =
     1.6    Isabelle_Process.protocol_command "Simplifier_Trace.reply"
     1.7 -    (fn [s, r] =>
     1.8 +    (fn [serial_string, reply] =>
     1.9        let
    1.10 -        val serial = Markup.parse_int s
    1.11 -        fun lookup_delete tab =
    1.12 -          (Inttab.lookup tab serial, Inttab.delete_safe serial tab)
    1.13 -        fun apply_result (SOME promise) = Future.fulfill promise r
    1.14 -          | apply_result NONE = () (* FIXME handle protocol failure, just like in active.ML? *)
    1.15 +        val serial = Markup.parse_int serial_string
    1.16 +        val result =
    1.17 +          Synchronized.change_result futures
    1.18 +            (fn tab => (Inttab.lookup tab serial, Inttab.delete_safe serial tab))
    1.19        in
    1.20 -        (Synchronized.change_result futures lookup_delete |> apply_result)
    1.21 -          handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn
    1.22 -      end)
    1.23 +        (case result of
    1.24 +          SOME promise => Future.fulfill promise reply
    1.25 +        | NONE => ()) (* FIXME handle protocol failure, just like in active.ML (!?) *)
    1.26 +      end handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn)
    1.27  
    1.28  
    1.29