equal
deleted
inserted
replaced
664 let |
664 let |
665 val _ = |
665 val _ = |
666 if not int andalso int_only then warning (command_msg "Interactive-only " tr) |
666 if not int andalso int_only then warning (command_msg "Interactive-only " tr) |
667 else (); |
667 else (); |
668 |
668 |
669 fun do_timing f x = (Output.info (command_msg "" tr); timeap f x); |
669 fun do_timing f x = (warning (command_msg "" tr); timeap f x); |
670 fun do_profiling f x = profile (! profiling) f x; |
670 fun do_profiling f x = profile (! profiling) f x; |
671 |
671 |
672 val (result, opt_exn) = |
672 val (result, opt_exn) = |
673 state |> (apply_trans int trans |
673 state |> (apply_trans int trans |
674 |> (if ! profiling > 0 then do_profiling else I) |
674 |> (if ! profiling > 0 then do_profiling else I) |