tuned signature;
authorwenzelm
Wed Sep 11 15:42:05 2013 +0200 (2013-09-11)
changeset 5353951157ee7f5ba
parent 53538 4e9e150422d5
child 53540 7903fe2c271b
tuned signature;
src/Pure/General/name_space.ML
src/Pure/Isar/class.ML
src/Tools/subtyping.ML
     1.1 --- a/src/Pure/General/name_space.ML	Wed Sep 11 15:30:12 2013 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Sep 11 15:42:05 2013 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4    val extern: Proof.context -> T -> string -> xstring
     1.5    val extern_ord: Proof.context -> T -> string * string -> order
     1.6    val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
     1.7 +  val pretty: Proof.context -> T -> string -> Pretty.T
     1.8    val hide: bool -> string -> T -> T
     1.9    val merge: T * T -> T
    1.10    type naming
    1.11 @@ -194,6 +195,8 @@
    1.12  
    1.13  fun markup_extern ctxt space name = (markup space name, extern ctxt space name);
    1.14  
    1.15 +fun pretty ctxt space name = Pretty.mark_str (markup_extern ctxt space name);
    1.16 +
    1.17  
    1.18  (* modify internals *)
    1.19  
     2.1 --- a/src/Pure/Isar/class.ML	Wed Sep 11 15:30:12 2013 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Wed Sep 11 15:42:05 2013 +0200
     2.3 @@ -182,14 +182,14 @@
     2.4  
     2.5      fun prt_param (c, ty) =
     2.6        Pretty.block
     2.7 -       [Pretty.mark_str (Name_Space.markup_extern ctxt const_space c), Pretty.str " ::",
     2.8 +       [Name_Space.pretty ctxt const_space c, Pretty.str " ::",
     2.9          Pretty.brk 1, Syntax.pretty_typ ctxt (Type.strip_sorts_dummy ty)];
    2.10  
    2.11      fun prt_entry class =
    2.12        Pretty.block
    2.13          ([Pretty.command "class", Pretty.brk 1,
    2.14 -          Pretty.mark_str (Name_Space.markup_extern ctxt class_space class), Pretty.str ":",
    2.15 -          Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
    2.16 +          Name_Space.pretty ctxt class_space class, Pretty.str ":", Pretty.fbrk,
    2.17 +          Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
    2.18            (case try (Axclass.get_info thy) class of
    2.19              NONE => []
    2.20            | SOME {params, ...} =>
     3.1 --- a/src/Tools/subtyping.ML	Wed Sep 11 15:30:12 2013 +0200
     3.2 +++ b/src/Tools/subtyping.ML	Wed Sep 11 15:42:05 2013 +0200
     3.3 @@ -1046,9 +1046,9 @@
     3.4      val tmaps =
     3.5        sort (Name_Space.extern_ord ctxt type_space o pairself #1)
     3.6          (Symtab.dest (tmaps_of ctxt));
     3.7 -    fun show_map (x, (t, _)) =
     3.8 +    fun show_map (c, (t, _)) =
     3.9        Pretty.block
    3.10 -       [Pretty.mark_str (Name_Space.markup_extern ctxt type_space x), Pretty.str ":",
    3.11 +       [Name_Space.pretty ctxt type_space c, Pretty.str ":",
    3.12          Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt t)];
    3.13    in
    3.14     [Pretty.big_list "coercions between base types:" (map show_coercion simple),