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) ""