tuned output to resemble input syntax more closely;
authorwenzelm
Sun May 03 20:04:38 2015 +0200 (2015-05-03)
changeset 6024909377954133b
parent 60248 f7e4294216d2
child 60250 baf2c8fddaa4
tuned output to resemble input syntax more closely;
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Sun May 03 18:51:26 2015 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sun May 03 20:04:38 2015 +0200
     1.3 @@ -732,22 +732,27 @@
     1.4      "apply some intro/elim rule");
     1.5  
     1.6  
     1.7 +
     1.8  (** diagnostics **)
     1.9  
    1.10 -fun pretty_specification thy c =
    1.11 -  if is_class thy c then
    1.12 +fun pretty_specification thy class =
    1.13 +  if is_class thy class then
    1.14      let
    1.15 -      val class_ctxt = init c thy;
    1.16 -      val class_space = Proof_Context.class_space class_ctxt;
    1.17 +      val class_ctxt = init class thy;
    1.18 +      val prt_class = Name_Space.pretty class_ctxt (Proof_Context.class_space class_ctxt);
    1.19 +
    1.20 +      val super_classes = Sign.minimize_sort thy (Sign.super_classes thy class);
    1.21  
    1.22        val fix_args =
    1.23 -        #params (Axclass.get_info thy c)
    1.24 +        #params (Axclass.get_info thy class)
    1.25          |> map (fn (c, T) => (Binding.name (Long_Name.base_name c), SOME T, NoSyn));
    1.26        val fixes = if null fix_args then [] else [Element.Fixes fix_args];
    1.27 -      val assumes = Locale.hyp_spec_of thy c;
    1.28 +      val assumes = Locale.hyp_spec_of thy class;
    1.29  
    1.30        val header =
    1.31 -        [Pretty.keyword1 "class", Pretty.brk 1, Name_Space.pretty class_ctxt class_space c];
    1.32 +        [Pretty.keyword1 "class", Pretty.brk 1, prt_class class, Pretty.str " =", Pretty.brk 1] @
    1.33 +        Pretty.separate " +" (map prt_class super_classes) @
    1.34 +        (if null super_classes then [] else [Pretty.str " +"]);
    1.35        val body =
    1.36          if null fixes andalso null assumes then []
    1.37          else