more substructural sharing to gain significant compression;

--- a/src/Pure/PIDE/xml.ML	Wed Sep 07 23:08:04 2011 +0200
+++ b/src/Pure/PIDE/xml.ML	Thu Sep 08 00:20:09 2011 +0200
@@ -229,20 +229,45 @@
 end;
 
 
-(** cache for partial sharing (strings only) **)
+(** 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 =
-      (case Symtab.lookup_key (! strings) s of
-        SOME (s', ()) => s'
-      | NONE => (Unsynchronized.change strings (Symtab.update (s, ())); 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 (Elem ((name, props), body)) =
-          Elem ((string name, map (pairself string) props), map tree body)
-      | tree (Text s) = Text (string 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;