# HG changeset patch # User wenzelm # Date 1315429684 -7200 # Node ID 05b8997899a26855ec72cf5bab952fddfa984730 # Parent 44db3e309060db450b0d6e1feb89ed6fe81d12a4 XML.cache for partial sharing (strings only); diff -r 44db3e309060 -r 05b8997899a2 src/Pure/PIDE/xml.ML --- a/src/Pure/PIDE/xml.ML Wed Sep 07 22:00:41 2011 +0200 +++ b/src/Pure/PIDE/xml.ML Wed Sep 07 23:08:04 2011 +0200 @@ -47,6 +47,7 @@ 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 @@ -228,6 +229,23 @@ end; +(** cache for partial sharing (strings only) **) + +fun cache () = + let + val strings = Unsynchronized.ref (Symtab.empty: unit Symtab.table); + + fun string s = + (case Symtab.lookup_key (! strings) s of + SOME (s', ()) => s' + | NONE => (Unsynchronized.change strings (Symtab.update (s, ())); s)); + + fun tree (Elem ((name, props), body)) = + Elem ((string name, map (pairself string) props), map tree body) + | tree (Text s) = Text (string s); + in tree end; + + (** XML as data representation language **) diff -r 44db3e309060 -r 05b8997899a2 src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Wed Sep 07 22:00:41 2011 +0200 +++ b/src/Pure/PIDE/xml.scala Wed Sep 07 23:08:04 2011 +0200 @@ -84,7 +84,8 @@ def content(body: Body): Iterator[String] = content_stream(body).iterator - /* pipe-lined cache for partial sharing */ + + /** cache for partial sharing (weak table) **/ class Cache(initial_size: Int = 131071, max_string: Int = 100) {