equal
deleted
inserted
replaced
226 (** Error reporting **) |
226 (** Error reporting **) |
227 |
227 |
228 fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table)) |
228 fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table)) |
229 |
229 |
230 fun pr_goals ctxt st = |
230 fun pr_goals ctxt st = |
231 Display.pretty_goals_aux (ProofContext.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st |
231 Display.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st |
232 |> Pretty.chunks |
232 |> Pretty.chunks |
233 |> Pretty.string_of |
233 |> Pretty.string_of |
234 |
234 |
235 fun row_index i = chr (i + 97) |
235 fun row_index i = chr (i + 97) |
236 fun col_index j = string_of_int (j + 1) |
236 fun col_index j = string_of_int (j + 1) |