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