# HG changeset patch
# User wenzelm
# Date 1208442648 -7200
# Node ID c07b1a90600cb99999c9ce491754f9dca142a92f
# Parent  a079f8f0080b05e2d0c1f5a74bfd1b910869dfd8
removed obsolete raw_str;
added mark;

diff -r a079f8f0080b -r c07b1a90600c src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Apr 17 16:30:48 2008 +0200
+++ b/src/Pure/General/pretty.ML	Thu Apr 17 16:30:48 2008 +0200
@@ -28,7 +28,6 @@
   val default_indent: string -> int -> output
   val add_mode: string -> (string -> int -> output) -> unit
   type T
-  val raw_str: output * int -> T
   val str: string -> T
   val brk: int -> T
   val fbrk: T
@@ -38,6 +37,7 @@
   val block: T list -> T
   val strs: string list -> T
   val markup: Markup.T -> T list -> T
+  val mark: Markup.T -> T -> T
   val keyword: string -> T
   val command: string -> T
   val markup_chunks: Markup.T -> T list -> T
@@ -118,7 +118,6 @@
 
 (** derived operations to create formatting expressions **)
 
-val raw_str = String;
 val str = String o Output.output_width;
 
 fun brk wd = Break (false, wd);
@@ -138,8 +137,9 @@
 val strs = block o breaks o map str;
 
 fun markup m prts = markup_block m (0, prts);
-fun keyword name = markup (Markup.keyword name) [str name];
-fun command name = markup (Markup.command name) [str name];
+fun mark m prt = markup m [prt];
+fun keyword name = mark (Markup.keyword name) (str name);
+fun command name = mark (Markup.command name) (str name);
 
 fun markup_chunks m prts = markup m (fbreaks prts);
 val chunks = markup_chunks Markup.none;