merged

--- a/bin/isabelle-process	Thu Dec 17 13:51:50 2009 -0800
+++ b/bin/isabelle-process	Thu Dec 17 23:44:48 2009 +0100
@@ -213,7 +213,7 @@
 
 NICE="nice"
 if [ -n "$WRAPPER_OUTPUT" ]; then
-  [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT"
+#  [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT"
   MLTEXT="$MLTEXT; Isabelle_Process.init \"$WRAPPER_OUTPUT\";"
 elif [ -n "$PGIP" ]; then
   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"

--- a/src/Pure/General/xml.scala	Thu Dec 17 13:51:50 2009 -0800
+++ b/src/Pure/General/xml.scala	Thu Dec 17 23:44:48 2009 +0100
@@ -6,8 +6,11 @@
 
 package isabelle
 
+import java.util.WeakHashMap
+import java.lang.ref.WeakReference
+import javax.xml.parsers.DocumentBuilderFactory
+
 import org.w3c.dom.{Node, Document}
-import javax.xml.parsers.DocumentBuilderFactory
 
 
 object XML
@@ -92,6 +95,56 @@
   }
 
 
+  /* cache for partial sharing -- NOT THREAD SAFE */
+
+  class Cache(initial_size: Int)
+  {
+    private val table = new WeakHashMap[Any, WeakReference[Any]](initial_size)
+
+    private def lookup[A](x: A): Option[A] =
+    {
+      val ref = table.get(x)
+      if (ref == null) None
+      else {
+        val y = ref.asInstanceOf[WeakReference[A]].get
+        if (y == null) None
+        else Some(y)
+      }
+    }
+    private def store[A](x: A): A =
+    {
+      table.put(x, new WeakReference[Any](x))
+      x
+    }
+
+    def cache_string(x: String): String =
+      lookup(x) match {
+        case Some(y) => y
+        case None => store(x)
+      }
+    def cache_props(x: List[(String, String)]): List[(String, String)] =
+      lookup(x) match {
+        case Some(y) => y
+        case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
+      }
+    def apply(x: XML.Tree): XML.Tree =
+      lookup(x) match {
+        case Some(y) => y
+        case None =>
+          x match {
+            case XML.Elem(name, props, body) =>
+              store(XML.Elem(cache_string(name), cache_props(props), apply(body)))
+            case XML.Text(text) => XML.Text(cache_string(text))
+          }
+      }
+    def apply(x: List[XML.Tree]): List[XML.Tree] =
+      lookup(x) match {
+        case Some(y) => y
+        case None => x.map(apply(_))
+      }
+  }
+
+
   /* document object model (W3C DOM) */
 
   def get_data(node: Node): Option[XML.Tree] =

--- a/src/Pure/IsaMakefile	Thu Dec 17 13:51:50 2009 -0800
+++ b/src/Pure/IsaMakefile	Thu Dec 17 23:44:48 2009 +0100
@@ -128,6 +128,7 @@
   System/cygwin.scala System/gui_setup.scala				\
   System/isabelle_process.scala System/isabelle_syntax.scala		\
   System/isabelle_system.scala System/platform.scala			\
+  /home/makarius/isabelle/misc/test_process/test.scala			\
   Thy/completion.scala Thy/html.scala Thy/thy_header.scala
 
 JAR_DIR = $(ISABELLE_HOME)/lib/classes

--- a/src/Pure/System/isabelle_process.scala	Thu Dec 17 13:51:50 2009 -0800
+++ b/src/Pure/System/isabelle_process.scala	Thu Dec 17 23:44:48 2009 +0100
@@ -100,6 +100,9 @@
     def is_raw = Kind.is_raw(kind)
     def is_control = Kind.is_control(kind)
     def is_system = Kind.is_system(kind)
+
+    def cache(table: XML.Cache): Result =
+      new Result(kind, table.cache_props(props), table(body))
   }
 }