src/Pure/PIDE/yxml.ML
changeset 49656 7ff712de5747
parent 46832 050e344825c8
child 59433 9da5b2c61049
     1.1 --- a/src/Pure/PIDE/yxml.ML	Sat Sep 29 13:43:23 2012 +0200
     1.2 +++ b/src/Pure/PIDE/yxml.ML	Sat Sep 29 16:15:18 2012 +0200
     1.3 @@ -23,6 +23,7 @@
     1.4    val output_markup: Markup.T -> string * string
     1.5    val string_of_body: XML.body -> string
     1.6    val string_of: XML.tree -> string
     1.7 +  val output_markup_elem: Markup.T -> (string * string) * string
     1.8    val parse_body: string -> XML.body
     1.9    val parse: string -> XML.tree
    1.10  end;
    1.11 @@ -75,6 +76,16 @@
    1.12  val string_of = string_of_body o single;
    1.13  
    1.14  
    1.15 +(* wrapped elements *)
    1.16 +
    1.17 +val Z = chr 0;
    1.18 +val Z_text = [XML.Text Z];
    1.19 +
    1.20 +fun output_markup_elem markup =
    1.21 +  let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
    1.22 +  in ((bg1, bg2), en) end;
    1.23 +
    1.24 +
    1.25  
    1.26  (** efficient YXML parsing **)
    1.27