180 val Ss = Sorts.mg_domain algebra tyco [class]; |
180 val Ss = Sorts.mg_domain algebra tyco [class]; |
181 in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; |
181 in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; |
182 |
182 |
183 fun prt_param (c, ty) = |
183 fun prt_param (c, ty) = |
184 Pretty.block |
184 Pretty.block |
185 [Pretty.mark_str (Name_Space.markup_extern ctxt const_space c), Pretty.str " ::", |
185 [Name_Space.pretty ctxt const_space c, Pretty.str " ::", |
186 Pretty.brk 1, Syntax.pretty_typ ctxt (Type.strip_sorts_dummy ty)]; |
186 Pretty.brk 1, Syntax.pretty_typ ctxt (Type.strip_sorts_dummy ty)]; |
187 |
187 |
188 fun prt_entry class = |
188 fun prt_entry class = |
189 Pretty.block |
189 Pretty.block |
190 ([Pretty.command "class", Pretty.brk 1, |
190 ([Pretty.command "class", Pretty.brk 1, |
191 Pretty.mark_str (Name_Space.markup_extern ctxt class_space class), Pretty.str ":", |
191 Name_Space.pretty ctxt class_space class, Pretty.str ":", Pretty.fbrk, |
192 Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @ |
192 Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @ |
193 (case try (Axclass.get_info thy) class of |
193 (case try (Axclass.get_info thy) class of |
194 NONE => [] |
194 NONE => [] |
195 | SOME {params, ...} => |
195 | SOME {params, ...} => |
196 [Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @ |
196 [Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @ |
197 (case Symtab.lookup arities class of |
197 (case Symtab.lookup arities class of |