added strip_blanks;
authorwenzelm
Wed Jan 31 22:14:53 2001 +0100 (2001-01-31)
changeset 110102c6559297be3
parent 11009 9e0ad9a5f9bb
child 11011 14b78c0c9f05
added strip_blanks;
src/Pure/General/symbol.ML
     1.1 --- a/src/Pure/General/symbol.ML	Wed Jan 31 16:35:46 2001 +0100
     1.2 +++ b/src/Pure/General/symbol.ML	Wed Jan 31 22:14:53 2001 +0100
     1.3 @@ -28,6 +28,7 @@
     1.4    val is_symbolic: symbol -> bool
     1.5    val is_printable: symbol -> bool
     1.6    val length: symbol list -> int
     1.7 +  val strip_blanks: string -> string
     1.8    val beginning: symbol list -> string
     1.9    val scan: string list -> symbol * string list
    1.10    val scanner: string -> (symbol list -> 'a * symbol list) -> symbol list -> 'a
    1.11 @@ -115,6 +116,9 @@
    1.12        Some s' => if s' = "long" orelse s' = "Long" then 2 else 1
    1.13      | None => 1)) + n) (0, ss);
    1.14  
    1.15 +fun strip_blanks s =
    1.16 +  implode (#1 (Library.take_suffix is_blank (#2 (Library.take_prefix is_blank (explode s)))));
    1.17 +
    1.18  
    1.19  (* beginning *)
    1.20