src/Pure/Isar/proof_display.ML
changeset 61261 ddb2da7cb2e4
parent 61258 2be9ea29f9ec
child 61266 eb9522a9d997
     1.1 --- a/src/Pure/Isar/proof_display.ML	Thu Sep 24 13:33:42 2015 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Thu Sep 24 23:33:29 2015 +0200
     1.3 @@ -82,25 +82,25 @@
     1.4  fun pretty_definitions verbose ctxt =
     1.5    let
     1.6      val thy = Proof_Context.theory_of ctxt;
     1.7 +    val context = Proof_Context.defs_context ctxt;
     1.8  
     1.9      val const_space = Proof_Context.const_space ctxt;
    1.10      val type_space = Proof_Context.type_space ctxt;
    1.11      val item_space = fn Defs.Const => const_space | Defs.Type => type_space;
    1.12      fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
    1.13  
    1.14 -    fun markup_extern_item (kind, name) =
    1.15 -      let val (markup, xname) = Name_Space.markup_extern ctxt (item_space kind) name
    1.16 -      in (markup, (kind, xname)) end;
    1.17 +    fun extern_item (kind, name) =
    1.18 +      let val xname = Name_Space.extern ctxt (item_space kind) name
    1.19 +      in (xname, (kind, name)) end;
    1.20  
    1.21 -    fun pretty_entry ((markup, (kind, xname)), args) =
    1.22 -      let
    1.23 -        val prt_prefix =
    1.24 -          if kind = Defs.Type then [Pretty.keyword1 "type", Pretty.brk 1] else [];
    1.25 -        val prt_item = Pretty.mark_str (markup, xname);
    1.26 -        val prt_args = Defs.pretty_args ctxt args;
    1.27 -      in Pretty.block (prt_prefix @ [prt_item] @ prt_args) end;
    1.28 +    fun extern_item_ord ((xname1, (kind1, _)), (xname2, (kind2, _))) =
    1.29 +      (case Defs.item_kind_ord (kind1, kind2) of
    1.30 +        EQUAL => string_ord (xname1, xname2)
    1.31 +      | ord => ord);
    1.32  
    1.33 -    fun sort_items f = sort (Defs.item_ord o apply2 (snd o f));
    1.34 +    fun sort_items f = sort (extern_item_ord o apply2 f);
    1.35 +
    1.36 +    fun pretty_entry ((_: string, item), args) = Defs.pretty_entry context (item, args);
    1.37  
    1.38      fun pretty_reduct (lhs, rhs) = Pretty.block
    1.39        ([pretty_entry lhs, Pretty.str "  ->", Pretty.brk 2] @
    1.40 @@ -115,12 +115,12 @@
    1.41      val (reds1, reds2) =
    1.42        filter_out (prune_item o #1 o #1) reducts
    1.43        |> map (fn (lhs, rhs) =>
    1.44 -        (apfst markup_extern_item lhs, map (apfst markup_extern_item) (filter_out (prune_item o fst) rhs)))
    1.45 +        (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs)))
    1.46        |> sort_items (#1 o #1)
    1.47        |> filter_out (null o #2)
    1.48        |> List.partition (Defs.plain_args o #2 o #1);
    1.49  
    1.50 -    val rests = restricts |> map (apfst (apfst markup_extern_item)) |> sort_items (#1 o #1);
    1.51 +    val rests = restricts |> map (apfst (apfst extern_item)) |> sort_items (#1 o #1);
    1.52    in
    1.53      Pretty.big_list "definitions:"
    1.54        (map (Pretty.text_fold o single)