print_theory: print abbreviations nicely;
authorwenzelm
Sat Apr 08 22:51:19 2006 +0200 (2006-04-08)
changeset 193654fd1246d7998
parent 19364 38799cfa34e5
child 19366 a2040baa9444
print_theory: print abbreviations nicely;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Sat Apr 08 22:51:17 2006 +0200
     1.2 +++ b/src/Pure/display.ML	Sat Apr 08 22:51:19 2006 +0200
     1.3 @@ -190,9 +190,12 @@
     1.4  
     1.5      val pretty_arities = List.concat o map (fn (t, ars) => map (prt_arity t) ars);
     1.6  
     1.7 -    fun pretty_const (c, (ty, rhs)) = Pretty.block
     1.8 -      ([Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty] @
     1.9 -        (case rhs of NONE => [] | SOME t => [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]));
    1.10 +    fun pretty_const (c, ty) = Pretty.block
    1.11 +      [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    1.12 +
    1.13 +    fun pretty_abbrev (c, (ty, t)) = Pretty.block
    1.14 +      [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty,
    1.15 +        Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t];
    1.16  
    1.17      fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term_no_vars t];
    1.18  
    1.19 @@ -205,7 +208,9 @@
    1.20      val tdecls = NameSpace.dest_table types;
    1.21      val arties = NameSpace.dest_table (Sign.type_space thy, arities);
    1.22      val cnsts = NameSpace.extern_table constants;
    1.23 -    val cnstrs = NameSpace.extern_table constraints |> map (apsnd (rpair NONE));
    1.24 +    val log_cnsts = List.mapPartial (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
    1.25 +    val abbrevs = List.mapPartial (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
    1.26 +    val cnstrs = NameSpace.extern_table constraints;
    1.27      val axms = NameSpace.extern_table axioms;
    1.28      val oras = NameSpace.extern_table oracles;
    1.29    in
    1.30 @@ -219,8 +224,9 @@
    1.31        Pretty.big_list "syntactic types:" (List.mapPartial (pretty_type true) tdecls),
    1.32        Pretty.big_list "logical types:" (List.mapPartial (pretty_type false) tdecls),
    1.33        Pretty.big_list "type arities:" (pretty_arities arties),
    1.34 -      Pretty.big_list "consts:" (map pretty_const cnsts),
    1.35 -      Pretty.big_list "const constraints:" (map pretty_const cnstrs),
    1.36 +      Pretty.big_list "logical consts:" (map pretty_const log_cnsts),
    1.37 +      Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
    1.38 +      Pretty.big_list "constraints:" (map pretty_const cnstrs),
    1.39        Pretty.big_list "axioms:" (map prt_axm axms),
    1.40        Pretty.strs ("oracles:" :: (map #1 oras))]
    1.41    end;