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.
tuned markup;
authorwenzelm
Fri, 14 Jan 2011 16:00:11 +0100
changeset 41551 791b139a6c1e
parent 41550 efa734d9b221
child 41552 c5e71fee3617
tuned markup;
src/Pure/Isar/proof_display.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/proof_display.ML	Fri Jan 14 15:44:47 2011 +0100
+++ b/src/Pure/Isar/proof_display.ML	Fri Jan 14 16:00:11 2011 +0100
@@ -80,12 +80,13 @@
 
 local
 
-fun pretty_fact_name (kind, "") = Pretty.str kind
-  | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
-      Pretty.str (Long_Name.base_name name), Pretty.str ":"];
+fun pretty_fact_name (kind, "") = Pretty.command kind
+  | pretty_fact_name (kind, name) =
+      Pretty.block [Pretty.command kind, Pretty.brk 1,
+        Pretty.str (Long_Name.base_name name), Pretty.str ":"];
 
 fun pretty_facts ctxt =
-  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
+  flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
     map (single o ProofContext.pretty_fact_aux ctxt false);
 
 in
isabelle