120 |
120 |
121 val cnsts = Name_Space.markup_entries verbose ctxt const_space constants; |
121 val cnsts = Name_Space.markup_entries verbose ctxt const_space constants; |
122 val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; |
122 val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; |
123 val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; |
123 val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; |
124 val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints; |
124 val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints; |
125 |
|
126 val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy); |
|
127 in |
125 in |
128 Pretty.chunks |
126 Pretty.chunks |
129 [Pretty.big_list "classes:" (map pretty_classrel clsses), |
127 [Pretty.big_list "classes:" (map pretty_classrel clsses), |
130 pretty_default default, |
128 pretty_default default, |
131 Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls), |
129 Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls), |
132 Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls), |
130 Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls), |
133 Pretty.big_list "type arities:" (pretty_arities arties), |
131 Pretty.big_list "type arities:" (pretty_arities arties), |
134 Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts), |
132 Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts), |
135 Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), |
133 Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), |
136 Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs), |
134 Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs), |
137 Pretty.big_list "axioms:" (map pretty_axm axms), |
|
138 Pretty.block |
135 Pretty.block |
139 (Pretty.breaks (Pretty.str "oracles:" :: |
136 (Pretty.breaks (Pretty.str "oracles:" :: |
140 map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))] |
137 map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))] |
141 end; |
138 end; |
142 |
139 |