# HG changeset patch
# User wenzelm
# Date 1636917328 -3600
# Node ID 4671d29feb00edc724e20b01eb6e30c5bf103426
# Parent  d2522bb4db1bf15c7160a0f6b969d6338c739217
tuned signature;

diff -r d2522bb4db1b -r 4671d29feb00 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sun Nov 14 17:46:41 2021 +0100
+++ b/src/Pure/PIDE/xml.ML	Sun Nov 14 20:15:28 2021 +0100
@@ -34,6 +34,7 @@
       Elem of (string * attributes) * tree list
     | Text of string
   type body = tree list
+  val string: string -> body
   val blob: string list -> body
   val is_empty: tree -> bool
   val is_empty_body: body -> bool
@@ -77,6 +78,9 @@
 
 open Output_Primitives.XML;
 
+fun string "" = []
+  | string s = [Text s];
+
 val blob = map Text;
 
 fun is_empty (Text "") = true
@@ -118,9 +122,7 @@
 fun trim_blanks trees =
   trees |> maps
     (fn Elem (markup, body) => [Elem (markup, trim_blanks body)]
-      | Text s =>
-          let val s' = s |> raw_explode |> trim Symbol.is_blank |> implode;
-          in if s' = "" then [] else [Text s'] end);
+      | Text s => s |> raw_explode |> trim Symbol.is_blank |> implode |> string);
 
 
 
diff -r d2522bb4db1b -r 4671d29feb00 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sun Nov 14 17:46:41 2021 +0100
+++ b/src/Pure/PIDE/xml.scala	Sun Nov 14 20:15:28 2021 +0100
@@ -44,6 +44,8 @@
   val no_text: Text = Text("")
   val newline: Text = Text("\n")
 
+  def string(s: String): Body = if (s.isEmpty) Nil else List(Text(s))
+
 
   /* name space */