--- a/src/Pure/PIDE/xml.ML Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Pure/PIDE/xml.ML Wed Mar 12 14:17:13 2014 +0100
@@ -37,6 +37,7 @@
val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option
val add_content: tree -> Buffer.T -> Buffer.T
val content_of: body -> string
+ val trim_blanks: body -> body
val header: string
val text: string -> string
val element: string -> attributes -> string list -> string
@@ -97,6 +98,21 @@
fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
+(* trim blanks *)
+
+fun trim_blanks trees =
+ trees |> maps
+ (fn Elem (markup, body) => [Elem (markup, trim_blanks body)]
+ | Text s =>
+ let
+ val s' = s
+ |> raw_explode
+ |> take_prefix Symbol.is_blank |> #2
+ |> take_suffix Symbol.is_blank |> #1
+ |> implode;
+ in if s' = "" then [] else [Text s'] end);
+
+
(** string representation **)