XML.cache for partial sharing (strings only);

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

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