--- 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 *)
--- 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;
--- 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);
--- 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 **)