src/Pure/PIDE/xml.ML

--- a/src/Pure/PIDE/xml.ML	Thu Nov 19 22:21:51 2015 +0100
+++ b/src/Pure/PIDE/xml.ML	Thu Nov 19 22:35:10 2015 +0100
@@ -104,12 +104,7 @@
   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;
+          let val s' = s |> raw_explode |> trim Symbol.is_blank |> implode;
           in if s' = "" then [] else [Text s'] end);