src/Pure/display.ML
changeset 14223 0ee05eef881b
parent 14178 14a12da7288e
child 14472 cba7c0a3ffb3
     1.1 --- a/src/Pure/display.ML	Wed Oct 08 16:02:54 2003 +0200
     1.2 +++ b/src/Pure/display.ML	Thu Oct 09 18:13:32 2003 +0200
     1.3 @@ -213,6 +213,11 @@
     1.4  
     1.5      fun pretty_arities (t, ars) = map (prt_arity t) ars;
     1.6  
     1.7 +    fun pretty_final (c:string, tys:typ list) = Pretty.block
     1.8 +      ([Pretty.str c, Pretty.str " ::", Pretty.brk 1] @
     1.9 +         (if null tys then [Pretty.str "<all instances>"]
    1.10 +	  else Pretty.commas (map prt_typ_no_tvars tys)));
    1.11 +
    1.12      fun pretty_const (c, ty) = Pretty.block
    1.13        [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    1.14  
    1.15 @@ -224,6 +229,7 @@
    1.16      val spaces' = Library.sort_wrt fst spaces;
    1.17      val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} =
    1.18        Type.rep_tsig tsig;
    1.19 +    val finals = Symtab.dest (#final_consts (rep_theory thy));
    1.20      val tycons = Sign.cond_extern_table sg Sign.typeK type_tab;
    1.21      val consts = Sign.cond_extern_table sg Sign.constK const_tab;
    1.22      val axms = Sign.cond_extern_table sg Theory.axiomK axioms;
    1.23 @@ -242,6 +248,7 @@
    1.24        Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)),
    1.25        Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))),
    1.26        Pretty.big_list "consts:" (map pretty_const consts),
    1.27 +      Pretty.big_list "finals:" (map pretty_final finals),
    1.28        Pretty.big_list "axioms:" (map prt_axm axms),
    1.29        Pretty.strs ("oracles:" :: (map #1 oras))]
    1.30    end;