# HG changeset patch
# User wenzelm
# Date 980975693 -3600
# Node ID 2c6559297be3fc1b444f87b8f7c003db4c71f60c
# Parent  9e0ad9a5f9bb7c194734e2a4a4ad58100f367b0b
added strip_blanks;

diff -r 9e0ad9a5f9bb -r 2c6559297be3 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Jan 31 16:35:46 2001 +0100
+++ b/src/Pure/General/symbol.ML	Wed Jan 31 22:14:53 2001 +0100
@@ -28,6 +28,7 @@
   val is_symbolic: symbol -> bool
   val is_printable: symbol -> bool
   val length: symbol list -> int
+  val strip_blanks: string -> string
   val beginning: symbol list -> string
   val scan: string list -> symbol * string list
   val scanner: string -> (symbol list -> 'a * symbol list) -> symbol list -> 'a
@@ -115,6 +116,9 @@
       Some s' => if s' = "long" orelse s' = "Long" then 2 else 1
     | None => 1)) + n) (0, ss);
 
+fun strip_blanks s =
+  implode (#1 (Library.take_suffix is_blank (#2 (Library.take_prefix is_blank (explode s)))));
+
 
 (* beginning *)