From d5b6e2668069721d91acb7fbcd0b2a92e08ce71e Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 10 Jun 2014 10:58:22 -0400 Subject: String.trim; add OnChange to more tags --- lib/ur/string.ur | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'lib/ur/string.ur') diff --git a/lib/ur/string.ur b/lib/ur/string.ur index 59a8e5c5..d760ec2b 100644 --- a/lib/ur/string.ur +++ b/lib/ur/string.ur @@ -86,3 +86,28 @@ fun newlines [ctx] [[Body] ~ ctx] (s : string) : xml ([Body] ++ ctx) [] [] = fun isPrefix {Full = f, Prefix = p} = length f >= length p && substring f {Start = 0, Len = length p} = p + +fun trim s = + let + val len = length s + + fun findStart i = + if i < len && Char.isSpace (sub s i) then + findStart (i+1) + else + i + + fun findFinish i = + if i >= 0 && Char.isSpace (sub s i) then + findFinish (i-1) + else + i + + val start = findStart 0 + val finish = findFinish (len - 1) + in + if finish >= start then + substring s {Start = start, Len = finish - start + 1} + else + "" + end -- cgit v1.2.3 From fb7713fd8543d1a42357d045d14909ba233151e0 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 11 Jun 2014 08:31:14 -0400 Subject: Change String to avoid Char dependency --- lib/ur/string.ur | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib/ur/string.ur') diff --git a/lib/ur/string.ur b/lib/ur/string.ur index d760ec2b..da4e7eb4 100644 --- a/lib/ur/string.ur +++ b/lib/ur/string.ur @@ -92,13 +92,13 @@ fun trim s = val len = length s fun findStart i = - if i < len && Char.isSpace (sub s i) then + if i < len && isspace (sub s i) then findStart (i+1) else i fun findFinish i = - if i >= 0 && Char.isSpace (sub s i) then + if i >= 0 && isspace (sub s i) then findFinish (i-1) else i -- cgit v1.2.3