tuned;
authorwenzelm
Thu Nov 19 22:35:10 2015 +0100 (2015-11-19)
changeset 61707d5ddd022a451
parent 61706 a1510dfb9bfa
child 61708 4de2380ae3ab
child 61709 47f7263870a0
tuned;
src/Pure/General/symbol.ML
src/Pure/General/symbol_pos.ML
src/Pure/PIDE/xml.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/General/symbol.ML	Thu Nov 19 22:21:51 2015 +0100
     1.2 +++ b/src/Pure/General/symbol.ML	Thu Nov 19 22:35:10 2015 +0100
     1.3 @@ -510,11 +510,7 @@
     1.4  
     1.5  (* blanks *)
     1.6  
     1.7 -fun trim_blanks s =
     1.8 -  sym_explode s
     1.9 -  |> take_prefix is_blank |> #2
    1.10 -  |> take_suffix is_blank |> #1
    1.11 -  |> implode;
    1.12 +val trim_blanks = sym_explode #> trim is_blank #> implode;
    1.13  
    1.14  
    1.15  (* bump string -- treat as base 26 or base 1 numbers *)
     2.1 --- a/src/Pure/General/symbol_pos.ML	Thu Nov 19 22:21:51 2015 +0100
     2.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Nov 19 22:35:10 2015 +0100
     2.3 @@ -74,9 +74,7 @@
     2.4            | (line, nl :: rest) => line :: split rest);
     2.5        in split list end;
     2.6  
     2.7 -val trim_blanks =
     2.8 -  take_prefix (Symbol.is_blank o symbol) #> #2 #>
     2.9 -  take_suffix (Symbol.is_blank o symbol) #> #1;
    2.10 +val trim_blanks = trim (Symbol.is_blank o symbol);
    2.11  
    2.12  val trim_lines =
    2.13    split_lines #> map trim_blanks #> separate [(Symbol.space, Position.none)] #> flat;
     3.1 --- a/src/Pure/PIDE/xml.ML	Thu Nov 19 22:21:51 2015 +0100
     3.2 +++ b/src/Pure/PIDE/xml.ML	Thu Nov 19 22:35:10 2015 +0100
     3.3 @@ -104,12 +104,7 @@
     3.4    trees |> maps
     3.5      (fn Elem (markup, body) => [Elem (markup, trim_blanks body)]
     3.6        | Text s =>
     3.7 -          let
     3.8 -            val s' = s
     3.9 -              |> raw_explode
    3.10 -              |> take_prefix Symbol.is_blank |> #2
    3.11 -              |> take_suffix Symbol.is_blank |> #1
    3.12 -              |> implode;
    3.13 +          let val s' = s |> raw_explode |> trim Symbol.is_blank |> implode;
    3.14            in if s' = "" then [] else [Text s'] end);
    3.15  
    3.16  
     4.1 --- a/src/Pure/library.ML	Thu Nov 19 22:21:51 2015 +0100
     4.2 +++ b/src/Pure/library.ML	Thu Nov 19 22:35:10 2015 +0100
     4.3 @@ -113,6 +113,7 @@
     4.4    val prefixes: 'a list -> 'a list list
     4.5    val suffixes1: 'a list -> 'a list list
     4.6    val suffixes: 'a list -> 'a list list
     4.7 +  val trim: ('a -> bool) -> 'a list -> 'a list
     4.8  
     4.9    (*integers*)
    4.10    val upto: int * int -> int list
    4.11 @@ -587,6 +588,7 @@
    4.12  fun suffixes1 xs = map rev (prefixes1 (rev xs));
    4.13  fun suffixes xs = [] :: suffixes1 xs;
    4.14  
    4.15 +fun trim pred = take_prefix pred #> #2 #> take_suffix pred #> #1;
    4.16  
    4.17  
    4.18  (** integers **)