Remove trailing newlines in outputs of X -where

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11768 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index fe715f0a7..93032140c 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -59,6 +59,9 @@ let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z')
 let is_digit c = (c >= '0' && c <= '9')
 let is_ident_tail c =
   is_letter c or is_digit c or c = '\'' or c = '_'
+let is_blank = function
+  | ' ' | '\r' | '\t' | '\n' -> true
+  | _ -> false
 
 (* Strings *)
 
@@ -73,6 +76,21 @@ let explode s =
 
 let implode sl = String.concat "" sl
 
+let strip s =
+  let n = String.length s in
+  let rec lstrip_rec i =
+    if i < n && is_blank s.[i] then
+      lstrip_rec (i+1)
+    else i
+  in
+  let rec rstrip_rec i =
+    if i >= 0 && is_blank s.[i] then
+      rstrip_rec (i-1)
+    else i
+  in
+  let a = lstrip_rec 0 and b = rstrip_rec (n-1) in
+  String.sub s a (b-a+1)
+
 (* substring searching... *)
 
 (* gdzie = where, co = what *)