# HG changeset patch # User wenzelm # Date 1348681810 -7200 # Node ID e716209814b39652be593f0d4d39c6338b12d94c # Parent 7bc5fcc035645e18878d04c4d078c128094c83fa discontinued XML.cache experiment -- Poly/ML 5.5.0 RTS does online sharing better; diff -r 7bc5fcc03564 -r e716209814b3 src/Pure/PIDE/xml.ML --- a/src/Pure/PIDE/xml.ML Wed Sep 26 16:37:21 2012 +0200 +++ b/src/Pure/PIDE/xml.ML Wed Sep 26 19:50:10 2012 +0200 @@ -47,7 +47,6 @@ val parse_element: string list -> tree * string list val parse_document: string list -> tree * string list val parse: string -> tree - val cache: unit -> tree -> tree exception XML_ATOM of string exception XML_BODY of body structure Encode: XML_DATA_OPS @@ -229,48 +228,6 @@ end; -(** cache for substructural sharing **) - -fun tree_ord tu = - if pointer_eq tu then EQUAL - else - (case tu of - (Text _, Elem _) => LESS - | (Elem _, Text _) => GREATER - | (Text s, Text s') => fast_string_ord (s, s') - | (Elem e, Elem e') => - prod_ord - (prod_ord fast_string_ord (list_ord (prod_ord fast_string_ord fast_string_ord))) - (list_ord tree_ord) (e, e')); - -structure Treetab = Table(type key = tree val ord = tree_ord); - -fun cache () = - let - val strings = Unsynchronized.ref (Symtab.empty: unit Symtab.table); - val trees = Unsynchronized.ref (Treetab.empty: unit Treetab.table); - - fun string s = - if size s <= 1 then s - else - (case Symtab.lookup_key (! strings) s of - SOME (s', ()) => s' - | NONE => (Unsynchronized.change strings (Symtab.update (s, ())); s)); - - fun tree t = - (case Treetab.lookup_key (! trees) t of - SOME (t', ()) => t' - | NONE => - let - val t' = - (case t of - Elem ((a, ps), b) => Elem ((string a, map (pairself string) ps), map tree b) - | Text s => Text (string s)); - val _ = Unsynchronized.change trees (Treetab.update (t', ())); - in t' end); - in tree end; - - (** XML as data representation language **)