equal
deleted
inserted
replaced
434 val num_steps = add_proof_steps (steps_of_proof isar_proof) 0 |
434 val num_steps = add_proof_steps (steps_of_proof isar_proof) 0 |
435 in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end |
435 in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end |
436 else |
436 else |
437 []) @ |
437 []) @ |
438 (if do_preplay then |
438 (if do_preplay then |
439 [(if preplay_fail then "may fail, " else "") ^ |
439 [(if preplay_fail then "may fail, " else "") ^ string_of_ext_time preplay_time] |
440 string_of_preplay_time preplay_time] |
|
441 else |
440 else |
442 []) |
441 []) |
443 in |
442 in |
444 "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ |
443 "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ |
445 Active.sendback_markup [Markup.padding_command] isar_text |
444 Active.sendback_markup [Markup.padding_command] isar_text |