src/Pure/General/symbol.ML
changeset 33955 fff6f11b1f09
parent 33548 6d5dfa64b980
child 34095 c2f176a38448
     1.1 --- a/src/Pure/General/symbol.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/Pure/General/symbol.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -183,7 +183,7 @@
     1.4          val raw1 = raw0 o implode;
     1.5          val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
     1.6      
     1.7 -        fun encode cs = enc (Library.take_prefix raw_chr cs)
     1.8 +        fun encode cs = enc (take_prefix raw_chr cs)
     1.9          and enc ([], []) = []
    1.10            | enc (cs, []) = [raw1 cs]
    1.11            | enc ([], d :: ds) = raw2 d :: encode ds
    1.12 @@ -198,11 +198,11 @@
    1.13  
    1.14  fun beginning n cs =
    1.15    let
    1.16 -    val drop_blanks = #1 o Library.take_suffix is_ascii_blank;
    1.17 +    val drop_blanks = #1 o take_suffix is_ascii_blank;
    1.18      val all_cs = drop_blanks cs;
    1.19      val dots = if length all_cs > n then " ..." else "";
    1.20    in
    1.21 -    (drop_blanks (Library.take (n, all_cs))
    1.22 +    (drop_blanks (take n all_cs)
    1.23        |> map (fn c => if is_ascii_blank c then space else c)
    1.24        |> implode) ^ dots
    1.25    end;
    1.26 @@ -491,8 +491,8 @@
    1.27  
    1.28  fun strip_blanks s =
    1.29    sym_explode s
    1.30 -  |> Library.take_prefix is_blank |> #2
    1.31 -  |> Library.take_suffix is_blank |> #1
    1.32 +  |> take_prefix is_blank |> #2
    1.33 +  |> take_suffix is_blank |> #1
    1.34    |> implode;
    1.35  
    1.36  
    1.37 @@ -516,7 +516,7 @@
    1.38            then chr (ord s + 1) :: ss
    1.39            else "a" :: s :: ss;
    1.40  
    1.41 -    val (ss, qs) = apfst rev (Library.take_suffix is_quasi (sym_explode str));
    1.42 +    val (ss, qs) = apfst rev (take_suffix is_quasi (sym_explode str));
    1.43      val ss' = if symbolic_end ss then "'" :: ss else bump ss;
    1.44    in implode (rev ss' @ qs) end;
    1.45