# HG changeset patch
# User wenzelm
# Date 1182287759 -7200
# Node ID d0efa182109fda0dcac1b2d0a5f46b938da49360
# Parent  b74315510f85dcffe61d3871f8be1552bad005bd
profiling: observe no_timing;

diff -r b74315510f85 -r d0efa182109f src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jun 19 23:15:57 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jun 19 23:15:59 2007 +0200
@@ -680,7 +680,7 @@
 
     val (result, opt_exn) =
        state |> (apply_trans int pos trans
-        |> (if ! profiling > 0 then do_profiling else I)
+        |> (if ! profiling > 0 then do_profiling andalso not no_timing else I)
         |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
     val _ =
       if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: ! print_mode)