227 | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys)); |
227 | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys)); |
228 |
228 |
229 end; |
229 end; |
230 |
230 |
231 |
231 |
232 (** cache for partial sharing (strings only) **) |
232 (** cache for substructural sharing **) |
|
233 |
|
234 fun tree_ord tu = |
|
235 if pointer_eq tu then EQUAL |
|
236 else |
|
237 (case tu of |
|
238 (Text _, Elem _) => LESS |
|
239 | (Elem _, Text _) => GREATER |
|
240 | (Text s, Text s') => fast_string_ord (s, s') |
|
241 | (Elem e, Elem e') => |
|
242 prod_ord |
|
243 (prod_ord fast_string_ord (list_ord (prod_ord fast_string_ord fast_string_ord))) |
|
244 (list_ord tree_ord) (e, e')); |
|
245 |
|
246 structure Treetab = Table(type key = tree val ord = tree_ord); |
233 |
247 |
234 fun cache () = |
248 fun cache () = |
235 let |
249 let |
236 val strings = Unsynchronized.ref (Symtab.empty: unit Symtab.table); |
250 val strings = Unsynchronized.ref (Symtab.empty: unit Symtab.table); |
|
251 val trees = Unsynchronized.ref (Treetab.empty: unit Treetab.table); |
237 |
252 |
238 fun string s = |
253 fun string s = |
239 (case Symtab.lookup_key (! strings) s of |
254 if size s <= 1 then s |
240 SOME (s', ()) => s' |
255 else |
241 | NONE => (Unsynchronized.change strings (Symtab.update (s, ())); s)); |
256 (case Symtab.lookup_key (! strings) s of |
242 |
257 SOME (s', ()) => s' |
243 fun tree (Elem ((name, props), body)) = |
258 | NONE => (Unsynchronized.change strings (Symtab.update (s, ())); s)); |
244 Elem ((string name, map (pairself string) props), map tree body) |
259 |
245 | tree (Text s) = Text (string s); |
260 fun tree t = |
|
261 (case Treetab.lookup_key (! trees) t of |
|
262 SOME (t', ()) => t' |
|
263 | NONE => |
|
264 let |
|
265 val t' = |
|
266 (case t of |
|
267 Elem ((a, ps), b) => Elem ((string a, map (pairself string) ps), map tree b) |
|
268 | Text s => Text (string s)); |
|
269 val _ = Unsynchronized.change trees (Treetab.update (t', ())); |
|
270 in t' end); |
246 in tree end; |
271 in tree end; |
247 |
272 |
248 |
273 |
249 |
274 |
250 (** XML as data representation language **) |
275 (** XML as data representation language **) |