37 |
37 |
38 fun preplay_trace ctxt assmsp concl result = |
38 fun preplay_trace ctxt assmsp concl result = |
39 let |
39 let |
40 val ctxt = ctxt |> Config.put show_markup true |
40 val ctxt = ctxt |> Config.put show_markup true |
41 val assms = op @ assmsp |
41 val assms = op @ assmsp |
42 val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str |
42 val time = Pretty.str ("[" ^ string_of_play_outcome result ^ "]") |
43 val nr_of_assms = length assms |
43 val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms) |
44 val assms = assms |
44 val concl = Syntax.pretty_term ctxt concl |
45 |> map (Display.pretty_thm ctxt) |
|
46 |> (fn [] => Pretty.str "" |
|
47 | [a] => a |
|
48 | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms) (* Syntax.pretty_term!? *) |
|
49 val concl = concl |> Syntax.pretty_term ctxt |
|
50 val trace_list = [] |
|
51 |> cons concl |
|
52 |> nr_of_assms > 0 ? cons (Pretty.str "\<Longrightarrow>") |
|
53 |> cons assms |
|
54 |> cons time |
|
55 val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list) |
|
56 in |
45 in |
57 tracing (Pretty.string_of pretty_trace) |
46 tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl]))) |
58 end |
47 end |
59 |
48 |
60 fun take_time timeout tac arg = |
49 fun take_time timeout tac arg = |
61 let val timing = Timing.start () in |
50 let val timing = Timing.start () in |
62 (TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing))) |
51 (TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing))) |