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 message;
authorwenzelm
Sun, 23 Jun 2013 21:40:56 +0200
changeset 52431 7fa1245f50df
parent 52430 289e36c2870a
child 52432 c03090937c3b
tuned message;
src/Pure/Isar/locale.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/locale.ML	Sun Jun 23 21:23:36 2013 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Jun 23 21:40:56 2013 +0200
@@ -218,8 +218,8 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val morph' = morph $> export;
-    fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
-    fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
+    fun print_qual (qual, mandatory) = qual ^ (if mandatory then "!" else "?");
+    fun prt_quals qs = Pretty.str (space_implode "." (map print_qual qs));
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     fun prt_term' t =
       if Config.get ctxt show_types
isabelle