# HG changeset patch
# User wenzelm
# Date 1302190697 -7200
# Node ID f87e0be80a3f9a59368b559228d1c4e4f01d788a
# Parent  ffdaa07cf6cf793caf24ad9c6c1ad007c163a840
clarified Pretty.mark;
added Pretty.mark_str, Pretty.marks_str convenience;

diff -r ffdaa07cf6cf -r f87e0be80a3f src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Apr 06 23:17:45 2011 +0200
+++ b/src/Pure/General/pretty.ML	Thu Apr 07 17:38:17 2011 +0200
@@ -34,6 +34,8 @@
   val strs: string list -> T
   val markup: Markup.T -> T list -> T
   val mark: Markup.T -> T -> T
+  val mark_str: Markup.T * string -> T
+  val marks_str: Markup.T list * string -> T
   val keyword: string -> T
   val command: string -> T
   val markup_chunks: Markup.T -> T list -> T
@@ -138,9 +140,12 @@
 val strs = block o breaks o map str;
 
 fun markup m prts = markup_block m (0, prts);
-fun mark m prt = markup m [prt];
-fun keyword name = mark Markup.keyword (str name);
-fun command name = mark Markup.command (str name);
+fun mark m prt = if m = Markup.empty then prt else markup m [prt];
+fun mark_str (m, s) = mark m (str s);
+fun marks_str (ms, s) = fold_rev mark ms (str s);
+
+fun keyword name = mark_str (Markup.keyword, name);
+fun command name = mark_str (Markup.command, name);
 
 fun markup_chunks m prts = markup m (fbreaks prts);
 val chunks = markup_chunks Markup.empty;