# HG changeset patch
# User wenzelm
# Date 1447968910 -3600
# Node ID d5ddd022a4519ea67617ba27ed5f8ebf461919df
# Parent  a1510dfb9bfa10c0f139f05e1b50b658828c997c
tuned;

diff -r a1510dfb9bfa -r d5ddd022a451 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Nov 19 22:21:51 2015 +0100
+++ b/src/Pure/General/symbol.ML	Thu Nov 19 22:35:10 2015 +0100
@@ -510,11 +510,7 @@
 
 (* blanks *)
 
-fun trim_blanks s =
-  sym_explode s
-  |> take_prefix is_blank |> #2
-  |> take_suffix is_blank |> #1
-  |> implode;
+val trim_blanks = sym_explode #> trim is_blank #> implode;
 
 
 (* bump string -- treat as base 26 or base 1 numbers *)
diff -r a1510dfb9bfa -r d5ddd022a451 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Thu Nov 19 22:21:51 2015 +0100
+++ b/src/Pure/General/symbol_pos.ML	Thu Nov 19 22:35:10 2015 +0100
@@ -74,9 +74,7 @@
           | (line, nl :: rest) => line :: split rest);
       in split list end;
 
-val trim_blanks =
-  take_prefix (Symbol.is_blank o symbol) #> #2 #>
-  take_suffix (Symbol.is_blank o symbol) #> #1;
+val trim_blanks = trim (Symbol.is_blank o symbol);
 
 val trim_lines =
   split_lines #> map trim_blanks #> separate [(Symbol.space, Position.none)] #> flat;
diff -r a1510dfb9bfa -r d5ddd022a451 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);
 
 
diff -r a1510dfb9bfa -r d5ddd022a451 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Nov 19 22:21:51 2015 +0100
+++ b/src/Pure/library.ML	Thu Nov 19 22:35:10 2015 +0100
@@ -113,6 +113,7 @@
   val prefixes: 'a list -> 'a list list
   val suffixes1: 'a list -> 'a list list
   val suffixes: 'a list -> 'a list list
+  val trim: ('a -> bool) -> 'a list -> 'a list
 
   (*integers*)
   val upto: int * int -> int list
@@ -587,6 +588,7 @@
 fun suffixes1 xs = map rev (prefixes1 (rev xs));
 fun suffixes xs = [] :: suffixes1 xs;
 
+fun trim pred = take_prefix pred #> #2 #> take_suffix pred #> #1;
 
 
 (** integers **)