equal
deleted
inserted
replaced
78 |
78 |
79 fun str_of_node (Theory _) = "in theory mode" |
79 fun str_of_node (Theory _) = "in theory mode" |
80 | str_of_node (Proof _) = "in proof mode"; |
80 | str_of_node (Proof _) = "in proof mode"; |
81 |
81 |
82 fun print_ctxt thy = Pretty.writeln (Pretty.block |
82 fun print_ctxt thy = Pretty.writeln (Pretty.block |
83 [Pretty.str "Theory:", Pretty.brk 1, Pretty.str (PureThy.get_name thy), |
83 [Pretty.str "theory", Pretty.brk 1, Pretty.str (PureThy.get_name thy), |
84 Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy]); |
84 Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy]); |
85 |
85 |
86 fun print_node_ctxt (Theory thy) = print_ctxt thy |
86 fun print_node_ctxt (Theory thy) = print_ctxt thy |
87 | print_node_ctxt (Proof prf) = print_ctxt (Proof.theory_of (ProofHistory.current prf)); |
87 | print_node_ctxt (Proof prf) = print_ctxt (Proof.theory_of (ProofHistory.current prf)); |
88 |
88 |