diff src/ur/feed.ur @ 2:2ec84d349838

String processing optimization
author Adam Chlipala <adam@chlipala.net>
date Tue, 11 Jan 2011 14:05:34 -0500
parents 8de269c09617
children ea0ca570c121
line wrap: on
line diff
--- a/src/ur/feed.ur	Tue Jan 11 13:17:44 2011 -0500
+++ b/src/ur/feed.ur	Tue Jan 11 14:05:34 2011 -0500
@@ -135,13 +135,13 @@
                         None => return ()
                       | Some (_, xml) => recur xml state
                 else if xml <> "" && String.sub xml 0 = #"!" then
-                    if String.length xml >= 3 && String.sub xml 1 = #"-" && String.sub xml 2 = #"-" then
+                    if String.lengthGe xml 3 && String.sub xml 1 = #"-" && String.sub xml 2 = #"-" then
                         let
                             fun skipper xml =
                                 case String.split xml #"-" of
                                     None => xml
                                   | Some (_, xml) =>
-                                    if String.length xml >= 2 && String.sub xml 0 = #"-" && String.sub xml 1 = #"\x3E" then
+                                    if String.lengthGe xml 2 && String.sub xml 0 = #"-" && String.sub xml 1 = #"\x3E" then
                                         String.suffix xml 2
                                     else
                                         skipper xml
@@ -168,7 +168,7 @@
                                          None => (xml, acc, True)
                                        | Some (_, xml) => (xml, acc, True))
                                   | _ =>
-                                    if String.length xml >= 2 && Char.isSpace (String.sub xml 0) then
+                                    if String.lengthGe xml 2 && Char.isSpace (String.sub xml 0) then
                                         readAttrs (String.sub xml 0) (String.suffix xml 1) acc
                                     else if xml <> "" && String.sub xml 0 = #"\x3E" then
                                         (String.suffix xml 1, acc, False)
@@ -210,7 +210,7 @@
                                             case String.split xml #"]" of
                                                 None => (acc ^ xml, None)
                                               | Some (pre, xml) =>
-                                                if String.length xml >= 2 && String.sub xml 0 = #"]" && String.sub xml 1 = #"\x3E" then
+                                                if String.lengthGe xml 2 && String.sub xml 0 = #"]" && String.sub xml 1 = #"\x3E" then
                                                     (String.suffix xml 2, Some (acc ^ pre))
                                                 else
                                                     skipper xml (acc ^ "]" ^ pre)