src/Pure/Isar/toplevel.ML
changeset 37905 0cf799737f5f
parent 37865 3a6ec95a9f68
child 37906 4195727a1f6c
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jul 22 10:41:12 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jul 22 14:01:43 2010 +0200
     1.3 @@ -578,7 +578,9 @@
     1.4  
     1.5  (* post-transition hooks *)
     1.6  
     1.7 -local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
     1.8 +local
     1.9 +  val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list);
    1.10 +in
    1.11  
    1.12  fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
    1.13  fun get_hooks () = ! hooks;
    1.14 @@ -597,9 +599,10 @@
    1.15        fun do_profiling f x = profile (! profiling) f x;
    1.16  
    1.17        val (result, status) =
    1.18 -         state |> (apply_trans int trans
    1.19 -          |> (if ! profiling > 0 andalso not no_timing then do_profiling else I)
    1.20 -          |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
    1.21 +         state |>
    1.22 +          (apply_trans int trans
    1.23 +            |> (! profiling > 0 andalso not no_timing) ? do_profiling
    1.24 +            |> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing);
    1.25  
    1.26        val _ = if int andalso not (! quiet) andalso print then print_state false result else ();
    1.27      in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);