# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1294772734 18000
# Node ID 2ec84d349838b2bfc11cd6074f9ffdf9ac703dac
# Parent  8de269c09617f6ac385e1580c1caf958b94d8c56
String processing optimization

diff -r 8de269c09617 -r 2ec84d349838 src/ur/feed.ur
--- 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)