XML.cache for partial sharing (strings only);
authorwenzelm
Wed Sep 07 23:08:04 2011 +0200 (2011-09-07 ago)
changeset 4480805b8997899a2
parent 44807 44db3e309060
child 44809 df3626d1066e
XML.cache for partial sharing (strings only);
src/Pure/PIDE/xml.ML
src/Pure/PIDE/xml.scala
     1.1 --- a/src/Pure/PIDE/xml.ML	Wed Sep 07 22:00:41 2011 +0200
     1.2 +++ b/src/Pure/PIDE/xml.ML	Wed Sep 07 23:08:04 2011 +0200
     1.3 @@ -47,6 +47,7 @@
     1.4    val parse_element: string list -> tree * string list
     1.5    val parse_document: string list -> tree * string list
     1.6    val parse: string -> tree
     1.7 +  val cache: unit -> tree -> tree
     1.8    exception XML_ATOM of string
     1.9    exception XML_BODY of body
    1.10    structure Encode: XML_DATA_OPS
    1.11 @@ -228,6 +229,23 @@
    1.12  end;
    1.13  
    1.14  
    1.15 +(** cache for partial sharing (strings only) **)
    1.16 +
    1.17 +fun cache () =
    1.18 +  let
    1.19 +    val strings = Unsynchronized.ref (Symtab.empty: unit Symtab.table);
    1.20 +
    1.21 +    fun string s =
    1.22 +      (case Symtab.lookup_key (! strings) s of
    1.23 +        SOME (s', ()) => s'
    1.24 +      | NONE => (Unsynchronized.change strings (Symtab.update (s, ())); s));
    1.25 +
    1.26 +    fun tree (Elem ((name, props), body)) =
    1.27 +          Elem ((string name, map (pairself string) props), map tree body)
    1.28 +      | tree (Text s) = Text (string s);
    1.29 +  in tree end;
    1.30 +
    1.31 +
    1.32  
    1.33  (** XML as data representation language **)
    1.34  
     2.1 --- a/src/Pure/PIDE/xml.scala	Wed Sep 07 22:00:41 2011 +0200
     2.2 +++ b/src/Pure/PIDE/xml.scala	Wed Sep 07 23:08:04 2011 +0200
     2.3 @@ -84,7 +84,8 @@
     2.4    def content(body: Body): Iterator[String] = content_stream(body).iterator
     2.5  
     2.6  
     2.7 -  /* pipe-lined cache for partial sharing */
     2.8 +
     2.9 +  /** cache for partial sharing (weak table) **/
    2.10  
    2.11    class Cache(initial_size: Int = 131071, max_string: Int = 100)
    2.12    {