Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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, 02 Sep 2008 18:01:24 +0200
changeset 28087 a9cccdd9d521
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 file | annotate | diff | comparison | revisions
src/Pure/Isar/proof_display.ML file | annotate | diff | comparison | revisions 
--- 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;
 
--- 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
isabelle