more substructural sharing to gain significant compression;
authorwenzelm
Thu Sep 08 00:20:09 2011 +0200 (2011-09-08)
changeset 44809df3626d1066e
parent 44808 05b8997899a2
child 44820 7798deb6f8fa
more substructural sharing to gain significant compression;
src/Pure/PIDE/xml.ML
     1.1 --- a/src/Pure/PIDE/xml.ML	Wed Sep 07 23:08:04 2011 +0200
     1.2 +++ b/src/Pure/PIDE/xml.ML	Thu Sep 08 00:20:09 2011 +0200
     1.3 @@ -229,20 +229,45 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(** cache for partial sharing (strings only) **)
     1.8 +(** cache for substructural sharing **)
     1.9 +
    1.10 +fun tree_ord tu =
    1.11 +  if pointer_eq tu then EQUAL
    1.12 +  else
    1.13 +    (case tu of
    1.14 +      (Text _, Elem _) => LESS
    1.15 +    | (Elem _, Text _) => GREATER
    1.16 +    | (Text s, Text s') => fast_string_ord (s, s')
    1.17 +    | (Elem e, Elem e') =>
    1.18 +        prod_ord
    1.19 +          (prod_ord fast_string_ord (list_ord (prod_ord fast_string_ord fast_string_ord)))
    1.20 +          (list_ord tree_ord) (e, e'));
    1.21 +
    1.22 +structure Treetab = Table(type key = tree val ord = tree_ord);
    1.23  
    1.24  fun cache () =
    1.25    let
    1.26      val strings = Unsynchronized.ref (Symtab.empty: unit Symtab.table);
    1.27 +    val trees = Unsynchronized.ref (Treetab.empty: unit Treetab.table);
    1.28  
    1.29      fun string s =
    1.30 -      (case Symtab.lookup_key (! strings) s of
    1.31 -        SOME (s', ()) => s'
    1.32 -      | NONE => (Unsynchronized.change strings (Symtab.update (s, ())); s));
    1.33 +      if size s <= 1 then s
    1.34 +      else
    1.35 +        (case Symtab.lookup_key (! strings) s of
    1.36 +          SOME (s', ()) => s'
    1.37 +        | NONE => (Unsynchronized.change strings (Symtab.update (s, ())); s));
    1.38  
    1.39 -    fun tree (Elem ((name, props), body)) =
    1.40 -          Elem ((string name, map (pairself string) props), map tree body)
    1.41 -      | tree (Text s) = Text (string s);
    1.42 +    fun tree t =
    1.43 +      (case Treetab.lookup_key (! trees) t of
    1.44 +        SOME (t', ()) => t'
    1.45 +      | NONE =>
    1.46 +          let
    1.47 +            val t' =
    1.48 +              (case t of
    1.49 +                Elem ((a, ps), b) => Elem ((string a, map (pairself string) ps), map tree b)
    1.50 +              | Text s => Text (string s));
    1.51 +            val _ = Unsynchronized.change trees (Treetab.update (t', ()));
    1.52 +          in t' end);
    1.53    in tree end;
    1.54  
    1.55