104 map (Attrib.local_attribute (Proof.theory_of st)) srcs)); |
104 map (Attrib.local_attribute (Proof.theory_of st)) srcs)); |
105 |
105 |
106 fun print_thms (name, srcs) = Toplevel.keep (fn state => |
106 fun print_thms (name, srcs) = Toplevel.keep (fn state => |
107 let |
107 let |
108 val ths = map (Thm.transfer (Toplevel.theory_of state)) |
108 val ths = map (Thm.transfer (Toplevel.theory_of state)) |
109 (Toplevel.node_cases PureThy.get_thms (ProofContext.get_thms o Proof.context_of) |
109 (Toplevel.node_case PureThy.get_thms (ProofContext.get_thms o Proof.context_of) |
110 state name); |
110 state name); |
111 val ths' = Toplevel.node_cases global_attribs local_attribs state ths srcs; |
111 val ths' = Toplevel.node_case global_attribs local_attribs state ths srcs; |
112 in Display.print_thms ths' end); |
112 in Display.print_thms ths' end); |
113 |
113 |
114 |
114 |
115 (* print types, terms and props *) |
115 (* print types, terms and props *) |
116 |
116 |
121 |
121 |
122 |
122 |
123 fun print_type s = Toplevel.keep (fn state => |
123 fun print_type s = Toplevel.keep (fn state => |
124 let |
124 let |
125 val sign = Toplevel.sign_of state; |
125 val sign = Toplevel.sign_of state; |
126 val T = Toplevel.node_cases read_typ (ProofContext.read_typ o Proof.context_of) state s; |
126 val T = Toplevel.node_case read_typ (ProofContext.read_typ o Proof.context_of) state s; |
127 in Pretty.writeln (Pretty.quote (Sign.pretty_typ sign T)) end); |
127 in Pretty.writeln (Pretty.quote (Sign.pretty_typ sign T)) end); |
128 |
128 |
129 fun print_term s = Toplevel.keep (fn state => |
129 fun print_term s = Toplevel.keep (fn state => |
130 let |
130 let |
131 val sign = Toplevel.sign_of state; |
131 val sign = Toplevel.sign_of state; |
132 val t = Toplevel.node_cases (read_term (TVar (("'z", 0), logicS))) |
132 val t = Toplevel.node_case (read_term (TVar (("'z", 0), logicS))) |
133 (ProofContext.read_term o Proof.context_of) state s; |
133 (ProofContext.read_term o Proof.context_of) state s; |
134 val T = Term.type_of t; |
134 val T = Term.type_of t; |
135 in |
135 in |
136 Pretty.writeln (Pretty.block [Pretty.quote (Sign.pretty_term sign t), Pretty.fbrk, |
136 Pretty.writeln (Pretty.block [Pretty.quote (Sign.pretty_term sign t), Pretty.fbrk, |
137 Pretty.str "::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ sign T)]) |
137 Pretty.str "::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ sign T)]) |