cond_timeit: added message argument;
authorwenzelm
Mon Dec 17 23:26:27 2007 +0100 (2007-12-17)
changeset 25685c36e10812ae4
parent 25684 2b3cce7d22b8
child 25686 bfa774974b6c
cond_timeit: added message argument;
src/Pure/Isar/outer_syntax.ML
src/Pure/old_goals.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Dec 17 22:40:14 2007 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Dec 17 23:26:27 2007 +0100
     1.3 @@ -304,7 +304,7 @@
     1.4        |> Source.exhaust;
     1.5  
     1.6      val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
     1.7 -    val _ = cond_timeit time (fn () =>
     1.8 +    val _ = cond_timeit time "" (fn () =>
     1.9        ThyOutput.process_thy (#1 (get_lexicons ())) command_tags is_markup trs toks
    1.10        |> Buffer.content
    1.11        |> Present.theory_output name);
     2.1 --- a/src/Pure/old_goals.ML	Mon Dec 17 22:40:14 2007 +0100
     2.2 +++ b/src/Pure/old_goals.ML	Mon Dec 17 23:26:27 2007 +0100
     2.3 @@ -228,7 +228,7 @@
     2.4            (case Seq.pull (tac st0) of
     2.5                 SOME(st,_) => st
     2.6               | _ => error ("prove_goal: tactic failed"))
     2.7 -  in  mkresult (check, cond_timeit (!Output.timing) statef)  end
     2.8 +  in  mkresult (check, cond_timeit (!Output.timing) "" statef)  end
     2.9    handle e => (print_sign_exn_unit (#thy (rep_cterm chorn)) e;
    2.10                 writeln ("The exception above was raised for\n" ^
    2.11                        Display.string_of_cterm chorn); raise e);
    2.12 @@ -402,7 +402,7 @@
    2.13                         thy_error (Thm.theory_of_thm th, Thm.theory_of_thm th2));
    2.14         ((th2,ths2)::(th,ths)::pairs)));
    2.15  
    2.16 -fun by tac = cond_timeit (!Output.timing)
    2.17 +fun by tac = cond_timeit (!Output.timing) ""
    2.18      (fn() => make_command (by_com tac));
    2.19  
    2.20  (* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn.