src/Pure/display.ML
changeset 19702 2ab12e94156f
parent 19698 f48cfaacd92c
child 19703 9c84266e1d5f
     1.1 --- a/src/Pure/display.ML	Tue May 23 13:55:01 2006 +0200
     1.2 +++ b/src/Pure/display.ML	Tue May 23 13:55:02 2006 +0200
     1.3 @@ -207,8 +207,12 @@
     1.4  
     1.5      fun pretty_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term_no_vars t];
     1.6  
     1.7 +    fun pretty_finals reds = Pretty.block
     1.8 +      (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o #1) reds));
     1.9 +
    1.10      fun pretty_reduct (lhs, rhs) = Pretty.block
    1.11 -      ([prt_const' lhs, Pretty.str "  ->", Pretty.brk 2] @ Pretty.commas (map prt_const' rhs));
    1.12 +      ([prt_const' lhs, Pretty.str "  ->", Pretty.brk 2] @
    1.13 +        Pretty.commas (map prt_const' (sort_wrt #1 rhs)));
    1.14  
    1.15      fun pretty_restrict (const, name) =
    1.16        Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
    1.17 @@ -232,9 +236,11 @@
    1.18      val axms = NameSpace.extern_table axioms;
    1.19      val oras = NameSpace.extern_table oracles;
    1.20  
    1.21 -    val reds = reducts |> map_filter (fn (lhs, rhs) =>
    1.22 -      if null rhs then NONE
    1.23 -      else SOME (apfst extern_const lhs, map (apfst extern_const) rhs)) |> sort_wrt (#1 o #1);
    1.24 +    val (reds0, (reds1, reds2)) = reducts |> map (fn (lhs, rhs) =>
    1.25 +        (apfst extern_const lhs, map (apfst extern_const) rhs))
    1.26 +      |> sort_wrt (#1 o #1)
    1.27 +      |> List.partition (null o #2)
    1.28 +      ||> List.partition (Defs.plain_args o #2 o #1);
    1.29      val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
    1.30    in
    1.31      [Pretty.strs ("names:" :: Context.names_of thy),
    1.32 @@ -251,10 +257,12 @@
    1.33        Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
    1.34        Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
    1.35        Pretty.big_list "axioms:" (map pretty_axm axms),
    1.36 +      Pretty.strs ("oracles:" :: (map #1 oras)),
    1.37        Pretty.big_list "definitions:"
    1.38 -        [Pretty.big_list "open dependencies:" (map pretty_reduct reds),
    1.39 -         Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)],
    1.40 -      Pretty.strs ("oracles:" :: (map #1 oras))]
    1.41 +        [pretty_finals reds0,
    1.42 +         Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
    1.43 +         Pretty.big_list "overloaded:" (map pretty_reduct reds2),
    1.44 +         Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]]
    1.45    end;
    1.46  
    1.47