Mercurial > feed
comparison 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 |
comparison
equal
deleted
inserted
replaced
1:8de269c09617 | 2:2ec84d349838 |
---|---|
133 else if xml <> "" && String.sub xml 0 = #"?" then | 133 else if xml <> "" && String.sub xml 0 = #"?" then |
134 case String.split xml #"\x3E" of | 134 case String.split xml #"\x3E" of |
135 None => return () | 135 None => return () |
136 | Some (_, xml) => recur xml state | 136 | Some (_, xml) => recur xml state |
137 else if xml <> "" && String.sub xml 0 = #"!" then | 137 else if xml <> "" && String.sub xml 0 = #"!" then |
138 if String.length xml >= 3 && String.sub xml 1 = #"-" && String.sub xml 2 = #"-" then | 138 if String.lengthGe xml 3 && String.sub xml 1 = #"-" && String.sub xml 2 = #"-" then |
139 let | 139 let |
140 fun skipper xml = | 140 fun skipper xml = |
141 case String.split xml #"-" of | 141 case String.split xml #"-" of |
142 None => xml | 142 None => xml |
143 | Some (_, xml) => | 143 | Some (_, xml) => |
144 if String.length xml >= 2 && String.sub xml 0 = #"-" && String.sub xml 1 = #"\x3E" then | 144 if String.lengthGe xml 2 && String.sub xml 0 = #"-" && String.sub xml 1 = #"\x3E" then |
145 String.suffix xml 2 | 145 String.suffix xml 2 |
146 else | 146 else |
147 skipper xml | 147 skipper xml |
148 in | 148 in |
149 recur (skipper (String.suffix xml 3)) state | 149 recur (skipper (String.suffix xml 3)) state |
166 | #"/" => | 166 | #"/" => |
167 (case String.split xml #"\x3E" of | 167 (case String.split xml #"\x3E" of |
168 None => (xml, acc, True) | 168 None => (xml, acc, True) |
169 | Some (_, xml) => (xml, acc, True)) | 169 | Some (_, xml) => (xml, acc, True)) |
170 | _ => | 170 | _ => |
171 if String.length xml >= 2 && Char.isSpace (String.sub xml 0) then | 171 if String.lengthGe xml 2 && Char.isSpace (String.sub xml 0) then |
172 readAttrs (String.sub xml 0) (String.suffix xml 1) acc | 172 readAttrs (String.sub xml 0) (String.suffix xml 1) acc |
173 else if xml <> "" && String.sub xml 0 = #"\x3E" then | 173 else if xml <> "" && String.sub xml 0 = #"\x3E" then |
174 (String.suffix xml 1, acc, False) | 174 (String.suffix xml 1, acc, False) |
175 else if xml <> "" && String.sub xml 0 = #"/" then | 175 else if xml <> "" && String.sub xml 0 = #"/" then |
176 (case String.split xml #"\x3E" of | 176 (case String.split xml #"\x3E" of |
208 let | 208 let |
209 fun skipper xml acc = | 209 fun skipper xml acc = |
210 case String.split xml #"]" of | 210 case String.split xml #"]" of |
211 None => (acc ^ xml, None) | 211 None => (acc ^ xml, None) |
212 | Some (pre, xml) => | 212 | Some (pre, xml) => |
213 if String.length xml >= 2 && String.sub xml 0 = #"]" && String.sub xml 1 = #"\x3E" then | 213 if String.lengthGe xml 2 && String.sub xml 0 = #"]" && String.sub xml 1 = #"\x3E" then |
214 (String.suffix xml 2, Some (acc ^ pre)) | 214 (String.suffix xml 2, Some (acc ^ pre)) |
215 else | 215 else |
216 skipper xml (acc ^ "]" ^ pre) | 216 skipper xml (acc ^ "]" ^ pre) |
217 in | 217 in |
218 skipper (String.suffix xml 9) "" | 218 skipper (String.suffix xml 9) "" |