fixed extern;
authorwenzelm
Mon Oct 13 17:49:50 1997 +0200 (1997-10-13)
changeset 38554bdf32173f6f
parent 3854 762606a888fe
child 3856 177c64693954
fixed extern;
added str_of_classrel, str_of_arity, str_of_arity;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Mon Oct 13 17:49:08 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Oct 13 17:49:50 1997 +0200
     1.3 @@ -59,6 +59,9 @@
     1.4    val string_of_term: sg -> term -> string
     1.5    val string_of_typ: sg -> typ -> string
     1.6    val string_of_sort: sg -> sort -> string
     1.7 +  val str_of_sort: sg -> sort -> string
     1.8 +  val str_of_classrel: sg -> class * class -> string
     1.9 +  val str_of_arity: sg -> string * sort list * sort -> string
    1.10    val pprint_term: sg -> term -> pprint_args -> unit
    1.11    val pprint_typ: sg -> typ -> pprint_args -> unit
    1.12    val certify_typ: sg -> typ -> typ
    1.13 @@ -287,7 +290,7 @@
    1.14      map_typ I (mapping (intrn spaces typeK) add_typ_tycons T) T;
    1.15  
    1.16    val intern = intrn o spaces_of;
    1.17 -  val extern = intrn o spaces_of;
    1.18 +  val extern = extrn o spaces_of;
    1.19    val intern_class = intrn_class o spaces_of;
    1.20    val extern_class = extrn_class o spaces_of;
    1.21    val intern_sort = intrn_sort o spaces_of;
    1.22 @@ -388,11 +391,24 @@
    1.23    Syntax.pretty_sort syn
    1.24      (if ! long_names then S else extrn_sort spaces S);
    1.25  
    1.26 +fun pretty_classrel sg (c1, c2) = Pretty.block
    1.27 +  [pretty_sort sg [c1], Pretty.str " <", Pretty.brk 1, pretty_sort sg [c2]];
    1.28 +
    1.29 +fun pretty_arity sg (t, [], S) = Pretty.block
    1.30 +      [Pretty.str (t ^ " ::"), Pretty.brk 1, pretty_sort sg S]
    1.31 +  | pretty_arity sg (t, Ss, S) = Pretty.block
    1.32 +      [Pretty.str (t ^ " ::"), Pretty.brk 1,
    1.33 +        Pretty.list "(" ")" (map (pretty_sort sg) Ss),
    1.34 +        Pretty.brk 1, pretty_sort sg S];
    1.35  
    1.36  fun string_of_term sg t = Pretty.string_of (pretty_term sg t);
    1.37  fun string_of_typ sg T = Pretty.string_of (pretty_typ sg T);
    1.38  fun string_of_sort sg S = Pretty.string_of (pretty_sort sg S);
    1.39  
    1.40 +fun str_of_sort sg S = Pretty.str_of (pretty_sort sg S);
    1.41 +fun str_of_classrel sg c1_c2 = Pretty.str_of (pretty_classrel sg c1_c2);
    1.42 +fun str_of_arity sg ar = Pretty.str_of (pretty_arity sg ar);
    1.43 +
    1.44  fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
    1.45  fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg);
    1.46