# HG changeset patch
# User wenzelm
# Date 1348928118 -7200
# Node ID 7ff712de5747632877f3093a8246d476358be01f
# Parent  6642e559f165ab77a4583e936abffe7810b0c12e
treat wrapped markup elements as raw markup delimiters;

diff -r 6642e559f165 -r 7ff712de5747 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat Sep 29 13:43:23 2012 +0200
+++ b/src/Pure/General/pretty.ML	Sat Sep 29 16:15:18 2012 +0200
@@ -33,6 +33,7 @@
   val blk: int * T list -> T
   val block: T list -> T
   val strs: string list -> T
+  val raw_markup: Output.output * Output.output -> int * T list -> T
   val markup: Markup.T -> T list -> T
   val mark: Markup.T -> T -> T
   val mark_str: Markup.T * string -> T
@@ -61,9 +62,10 @@
   val output: int option -> T -> Output.output
   val string_of_margin: int -> T -> string
   val string_of: T -> string
+  val writeln: T -> unit
+  val symbolic_output: T -> Output.output
   val symbolic_string_of: T -> string
   val str_of: T -> string
-  val writeln: T -> unit
   val to_ML: T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
 end;
@@ -134,13 +136,13 @@
 fun breaks prts = Library.separate (brk 1) prts;
 fun fbreaks prts = Library.separate fbrk prts;
 
-fun block_markup m (indent, es) =
+fun raw_markup m (indent, es) =
   let
     fun sum [] k = k
       | sum (e :: es) k = sum es (length e + k);
   in Block (m, es, indent, sum es 0) end;
 
-fun markup_block m arg = block_markup (Markup.output m) arg;
+fun markup_block m arg = raw_markup (Markup.output m) arg;
 
 val blk = markup_block Markup.empty;
 fun block prts = blk (2, prts);
@@ -325,9 +327,12 @@
 val output = Buffer.content oo output_buffer;
 fun string_of_margin margin = Output.escape o output (SOME margin);
 val string_of = Output.escape o output NONE;
-val symbolic_string_of = Output.escape o Buffer.content o symbolic;
+val writeln = Output.writeln o string_of;
+
+val symbolic_output = Buffer.content o symbolic;
+val symbolic_string_of = Output.escape o symbolic_output;
+
 val str_of = Output.escape o Buffer.content o unformatted;
-val writeln = Output.writeln o string_of;
 
 
 
@@ -337,7 +342,7 @@
   | to_ML (String s) = ML_Pretty.String s
   | to_ML (Break b) = ML_Pretty.Break b;
 
-fun from_ML (ML_Pretty.Block (m, prts, ind)) = block_markup m (ind, map from_ML prts)
+fun from_ML (ML_Pretty.Block (m, prts, ind)) = raw_markup m (ind, map from_ML prts)
   | from_ML (ML_Pretty.String s) = String s
   | from_ML (ML_Pretty.Break b) = Break b;
 
diff -r 6642e559f165 -r 7ff712de5747 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Sep 29 13:43:23 2012 +0200
+++ b/src/Pure/PIDE/yxml.ML	Sat Sep 29 16:15:18 2012 +0200
@@ -23,6 +23,7 @@
   val output_markup: Markup.T -> string * string
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
+  val output_markup_elem: Markup.T -> (string * string) * string
   val parse_body: string -> XML.body
   val parse: string -> XML.tree
 end;
@@ -75,6 +76,16 @@
 val string_of = string_of_body o single;
 
 
+(* wrapped elements *)
+
+val Z = chr 0;
+val Z_text = [XML.Text Z];
+
+fun output_markup_elem markup =
+  let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
+  in ((bg1, bg2), en) end;
+
+
 
 (** efficient YXML parsing **)