src/Pure/library.ML
changeset 47499 4b0daca2bf88
parent 47060 e2741ec9ae36
child 48271 b28defd0b5a5
     1.1 --- a/src/Pure/library.ML	Mon Apr 16 21:53:11 2012 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Apr 16 23:07:40 2012 +0200
     1.3 @@ -150,6 +150,7 @@
     1.4    val suffix: string -> string -> string
     1.5    val unprefix: string -> string -> string
     1.6    val unsuffix: string -> string -> string
     1.7 +  val trim_line: string -> string
     1.8    val replicate_string: int -> string -> string
     1.9    val translate_string: (string -> string) -> string -> string
    1.10    val match_string: string -> string -> bool
    1.11 @@ -755,6 +756,8 @@
    1.12    if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
    1.13    else raise Fail "unsuffix";
    1.14  
    1.15 +val trim_line = perhaps (try (unsuffix "\n"));
    1.16 +
    1.17  fun replicate_string (0: int) _ = ""
    1.18    | replicate_string 1 a = a
    1.19    | replicate_string k a =