pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
authorwenzelm
Tue Sep 02 18:01:24 2008 +0200 (2008-09-02)
changeset 28087a9cccdd9d521
parent 28086 db584d1d2af4
child 28088 723735f2d73a
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Sep 02 18:01:23 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Sep 02 18:01:24 2008 +0200
     1.3 @@ -296,10 +296,10 @@
     1.4    | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
     1.5  
     1.6  fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
     1.7 -  | pretty_fact ctxt (a, [th]) =
     1.8 -      Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
     1.9 -  | pretty_fact ctxt (a, ths) =
    1.10 -      Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths));
    1.11 +  | pretty_fact ctxt (a, [th]) = Pretty.block
    1.12 +      [Pretty.str (NameSpace.base a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
    1.13 +  | pretty_fact ctxt (a, ths) = Pretty.block
    1.14 +      (Pretty.fbreaks (Pretty.str (NameSpace.base a ^ ":") :: map (pretty_thm ctxt) ths));
    1.15  
    1.16  val string_of_thm = Pretty.string_of oo pretty_thm;
    1.17  
     2.1 --- a/src/Pure/Isar/proof_display.ML	Tue Sep 02 18:01:23 2008 +0200
     2.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Sep 02 18:01:24 2008 +0200
     2.3 @@ -79,6 +79,10 @@
     2.4  
     2.5  (* results *)
     2.6  
     2.7 +fun pretty_fact_name (kind, "") = Pretty.str kind
     2.8 +  | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
     2.9 +      Pretty.str (NameSpace.base name), Pretty.str ":"];
    2.10 +
    2.11  local
    2.12  
    2.13  fun pretty_facts ctxt =
    2.14 @@ -87,11 +91,11 @@
    2.15  
    2.16  fun pretty_results ctxt ((kind, ""), facts) =
    2.17        Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts)
    2.18 -  | pretty_results ctxt ((kind, name), [fact]) = Pretty.blk (1,
    2.19 -      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
    2.20 -  | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
    2.21 -      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
    2.22 -        Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
    2.23 +  | pretty_results ctxt (kind_name, [fact]) = Pretty.blk (1,
    2.24 +      [pretty_fact_name kind_name, Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
    2.25 +  | pretty_results ctxt (kind_name, facts) = Pretty.blk (1,
    2.26 +      [pretty_fact_name kind_name, Pretty.fbrk, Pretty.blk (1,
    2.27 +        Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
    2.28  
    2.29  in
    2.30