# HG changeset patch
# User wenzelm
# Date 1220371284 -7200
# Node ID a9cccdd9d5217017f66df1b5ed79f5f09d784ac0
# Parent  db584d1d2af4a7ef778a4eae4e52266a5f4b42c0
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);

diff -r db584d1d2af4 -r a9cccdd9d521 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Sep 02 18:01:23 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Sep 02 18:01:24 2008 +0200
@@ -296,10 +296,10 @@
   | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
 
 fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
-  | pretty_fact ctxt (a, [th]) =
-      Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
-  | pretty_fact ctxt (a, ths) =
-      Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths));
+  | pretty_fact ctxt (a, [th]) = Pretty.block
+      [Pretty.str (NameSpace.base a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
+  | pretty_fact ctxt (a, ths) = Pretty.block
+      (Pretty.fbreaks (Pretty.str (NameSpace.base a ^ ":") :: map (pretty_thm ctxt) ths));
 
 val string_of_thm = Pretty.string_of oo pretty_thm;
 
diff -r db584d1d2af4 -r a9cccdd9d521 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Sep 02 18:01:23 2008 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Sep 02 18:01:24 2008 +0200
@@ -79,6 +79,10 @@
 
 (* results *)
 
+fun pretty_fact_name (kind, "") = Pretty.str kind
+  | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
+      Pretty.str (NameSpace.base name), Pretty.str ":"];
+
 local
 
 fun pretty_facts ctxt =
@@ -87,11 +91,11 @@
 
 fun pretty_results ctxt ((kind, ""), facts) =
       Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts)
-  | pretty_results ctxt ((kind, name), [fact]) = Pretty.blk (1,
-      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
-  | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
-      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
-        Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
+  | pretty_results ctxt (kind_name, [fact]) = Pretty.blk (1,
+      [pretty_fact_name kind_name, Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
+  | pretty_results ctxt (kind_name, facts) = Pretty.blk (1,
+      [pretty_fact_name kind_name, Pretty.fbrk, Pretty.blk (1,
+        Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
 
 in