50 (get_mets ())) |
50 (get_mets ())) |
51 |
51 |
52 |
52 |
53 (** show a whole Calc.T **) |
53 (** show a whole Calc.T **) |
54 |
54 |
55 fun posterm2str ctxt (pos, t, _) = "(" ^ Pos.pos'2str pos ^ ", " ^ UnparseC.term_in_ctxt ctxt t ^ ")" |
55 fun posterm2str ctxt (pos, t, _) = "(" ^ Pos.pos'2str pos ^ ", " ^ UnparseC.term ctxt t ^ ")" |
56 fun posterms2str ctxt pfs = (strs2str' o (map (curry op ^ "\n")) o (map (posterm2str ctxt))) pfs |
56 fun posterms2str ctxt pfs = (strs2str' o (map (curry op ^ "\n")) o (map (posterm2str ctxt))) pfs |
57 |
57 |
58 fun postermtac2str ctxt (pos, t, SOME tac) = |
58 fun postermtac2str ctxt (pos, t, SOME tac) = |
59 Pos.pos'2str pos ^ ", " ^ UnparseC.term_in_ctxt ctxt t ^ "\n" ^ |
59 Pos.pos'2str pos ^ ", " ^ UnparseC.term ctxt t ^ "\n" ^ |
60 indent 10 ^ Tactic.input_to_string ctxt tac |
60 indent 10 ^ Tactic.input_to_string ctxt tac |
61 | postermtac2str ctxt (pos, t, NONE) = |
61 | postermtac2str ctxt (pos, t, NONE) = |
62 Pos.pos'2str pos ^ ", " ^ UnparseC.term_in_ctxt ctxt t |
62 Pos.pos'2str pos ^ ", " ^ UnparseC.term ctxt t |
63 fun postermtacs2str ctxt pfts = |
63 fun postermtacs2str ctxt pfts = |
64 (strs2str' o (map (curry op ^ "\n")) o (map (postermtac2str ctxt))) pfts |
64 (strs2str' o (map (curry op ^ "\n")) o (map (postermtac2str ctxt))) pfts |
65 |
65 |
66 (* WN050225 shows a WRONG last step, if pt is incomplete *) |
66 (* WN050225 shows a WRONG last step, if pt is incomplete *) |
67 fun show_pt pt = |
67 fun show_pt pt = |