Mercurial > feed
changeset 2:2ec84d349838
String processing optimization
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 11 Jan 2011 14:05:34 -0500 |
| parents | 8de269c09617 |
| children | ea0ca570c121 |
| files | src/ur/feed.ur |
| diffstat | 1 files changed, 4 insertions(+), 4 deletions(-) [+] |
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)