18 val pwd: Toplevel.transition -> Toplevel.transition |
18 val pwd: Toplevel.transition -> Toplevel.transition |
19 val use_thy: string -> Toplevel.transition -> Toplevel.transition |
19 val use_thy: string -> Toplevel.transition -> Toplevel.transition |
20 val load: string -> Toplevel.transition -> Toplevel.transition |
20 val load: string -> Toplevel.transition -> Toplevel.transition |
21 val print_theory: Toplevel.transition -> Toplevel.transition |
21 val print_theory: Toplevel.transition -> Toplevel.transition |
22 val print_syntax: Toplevel.transition -> Toplevel.transition |
22 val print_syntax: Toplevel.transition -> Toplevel.transition |
|
23 val print_theorems: Toplevel.transition -> Toplevel.transition |
23 val print_attributes: Toplevel.transition -> Toplevel.transition |
24 val print_attributes: Toplevel.transition -> Toplevel.transition |
24 val print_methods: Toplevel.transition -> Toplevel.transition |
25 val print_methods: Toplevel.transition -> Toplevel.transition |
25 val print_binds: Toplevel.transition -> Toplevel.transition |
26 val print_binds: Toplevel.transition -> Toplevel.transition |
26 val print_lthms: Toplevel.transition -> Toplevel.transition |
27 val print_lthms: Toplevel.transition -> Toplevel.transition |
27 val print_thms: xstring -> Toplevel.transition -> Toplevel.transition |
28 val print_thms: xstring * Args.src list -> Toplevel.transition -> Toplevel.transition |
28 val print_prop: string -> Toplevel.transition -> Toplevel.transition |
29 val print_prop: string -> Toplevel.transition -> Toplevel.transition |
29 val print_term: string -> Toplevel.transition -> Toplevel.transition |
30 val print_term: string -> Toplevel.transition -> Toplevel.transition |
30 val print_type: string -> Toplevel.transition -> Toplevel.transition |
31 val print_type: string -> Toplevel.transition -> Toplevel.transition |
31 end; |
32 end; |
32 |
33 |
79 |
80 |
80 (* print theory contents *) |
81 (* print theory contents *) |
81 |
82 |
82 val print_theory = Toplevel.keep (PureThy.print_theory o Toplevel.theory_of); |
83 val print_theory = Toplevel.keep (PureThy.print_theory o Toplevel.theory_of); |
83 val print_syntax = Toplevel.keep (Display.print_syntax o Toplevel.theory_of); |
84 val print_syntax = Toplevel.keep (Display.print_syntax o Toplevel.theory_of); |
|
85 val print_theorems = Toplevel.keep (PureThy.print_theorems o Toplevel.theory_of); |
84 val print_attributes = Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); |
86 val print_attributes = Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); |
85 val print_methods = Toplevel.keep (Method.print_methods o Toplevel.theory_of); |
87 val print_methods = Toplevel.keep (Method.print_methods o Toplevel.theory_of); |
86 |
88 |
87 |
89 |
88 (* print proof context contents *) |
90 (* print proof context contents *) |
91 val print_lthms = Toplevel.keep (ProofContext.print_thms o Proof.context_of o Toplevel.proof_of); |
93 val print_lthms = Toplevel.keep (ProofContext.print_thms o Proof.context_of o Toplevel.proof_of); |
92 |
94 |
93 |
95 |
94 (* print theorems *) |
96 (* print theorems *) |
95 |
97 |
96 fun print_thms name = Toplevel.keep (fn state => |
98 fun global_attribs thy ths srcs = |
|
99 #2 (Attribute.applys ((Theory.copy thy, ths), map (Attrib.global_attribute thy) srcs)); |
|
100 |
|
101 fun local_attribs st ths srcs = |
|
102 #2 (Attribute.applys ((Proof.context_of st, ths), |
|
103 map (Attrib.local_attribute (Proof.theory_of st)) srcs)); |
|
104 |
|
105 fun print_thms (name, srcs) = Toplevel.keep (fn state => |
97 let |
106 let |
98 val prt_tthm = Attribute.pretty_tthm; |
107 val prt_tthm = Attribute.pretty_tthm; |
99 fun prt_tthms [th] = prt_tthm th |
108 fun prt_tthms [th] = prt_tthm th |
100 | prt_tthms ths = Pretty.block (Pretty.fbreaks (map prt_tthm ths)); |
109 | prt_tthms ths = Pretty.block (Pretty.fbreaks (map prt_tthm ths)); |
101 |
110 |
102 val tthms = map (apfst (Thm.transfer (Toplevel.theory_of state))) |
111 val ths = map (apfst (Thm.transfer (Toplevel.theory_of state))) |
103 (Toplevel.node_cases PureThy.get_tthms (ProofContext.get_tthms o Proof.context_of) |
112 (Toplevel.node_cases PureThy.get_tthms (ProofContext.get_tthms o Proof.context_of) |
104 state name); |
113 state name); |
105 in Pretty.writeln (prt_tthms tthms) end); |
114 val ths' = Toplevel.node_cases global_attribs local_attribs state ths srcs; |
|
115 in Pretty.writeln (prt_tthms ths') end); |
106 |
116 |
107 |
117 |
108 (* print types, terms and props *) |
118 (* print types, terms and props *) |
109 |
119 |
110 fun read_typ thy = Sign.read_typ (Theory.sign_of thy, K None); |
120 fun read_typ thy = Sign.read_typ (Theory.sign_of thy, K None); |