# HG changeset patch
# User blanchet
# Date 1261134044 -3600
# Node ID 85257fa296f6e98ed83d6147226e7563bcbe36d9
# Parent  b1cabadf68811842cff7287d1ae30585bea636a6# Parent  8a2c5d7aff51f7938bd06a1cfb1647a41f81237e
merged

diff -r 8a2c5d7aff51 -r 85257fa296f6 bin/isabelle-process
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Dec 18 12:00:29 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Dec 18 12:00:44 2009 +0100
@@ -204,6 +204,9 @@
   qed
 qed
 
+lemma rev_finite_subset: "finite B ==> A \<subseteq> B ==> finite A"
+by (rule finite_subset)
+
 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
 by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
 
@@ -355,6 +358,18 @@
   apply (simp add: finite_Un finite_subset [OF inj_vimage_singleton])
   done
 
+lemma finite_vimageD:
+  assumes fin: "finite (h -` F)" and surj: "surj h"
+  shows "finite F"
+proof -
+  have "finite (h ` (h -` F))" using fin by (rule finite_imageI)
+  also have "h ` (h -` F) = F" using surj by (rule surj_image_vimage_eq)
+  finally show "finite F" .
+qed
+
+lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
+  unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
+
 
 text {* The finite UNION of finite sets *}
 
@@ -2052,6 +2067,9 @@
 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)"
   by auto
 
+lemma card_gt_0_iff: "(0 < card A) = (A \<noteq> {} & finite A)"
+  by (simp add: neq0_conv [symmetric] card_eq_0_iff) 
+
 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A"
 apply(rule_tac t = A in insert_Diff [THEN subst], assumption)
 apply(simp del:insert_Diff_single)
@@ -2108,6 +2126,14 @@
   "finite B ==> B <= A ==> card (A - B) = card A - card B"
 by(simp add:card_def setsum_diff_nat)
 
+lemma card_Diff_subset_Int:
+  assumes AB: "finite (A \<inter> B)" shows "card (A - B) = card A - card (A \<inter> B)"
+proof -
+  have "A - B = A - A \<inter> B" by auto
+  thus ?thesis
+    by (simp add: card_Diff_subset AB) 
+qed
+
 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A"
 apply (rule Suc_less_SucD)
 apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Fri Dec 18 12:00:29 2009 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Dec 18 12:00:44 2009 +0100
@@ -371,21 +371,38 @@
   Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
   Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
 
-lemma INFM_EX:
-  "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
-  unfolding Inf_many_def
-proof (rule ccontr)
-  assume inf: "infinite {x. P x}"
-  assume "\<not> ?thesis" then have "{x. P x} = {}" by simp
-  then have "finite {x. P x}" by simp
-  with inf show False by simp
-qed
+lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}"
+  unfolding Inf_many_def ..
+
+lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}"
+  unfolding Alm_all_def Inf_many_def by simp
+
+(* legacy name *)
+lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
+
+lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
+  unfolding Alm_all_def not_not ..
 
-lemma MOST_iff_finiteNeg: "(\<forall>\<^sub>\<infinity>x. P x) = finite {x. \<not> P x}"
-  by (simp add: Alm_all_def Inf_many_def)
+lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
+  unfolding Alm_all_def not_not ..
+
+lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
+  unfolding Inf_many_def by simp
+
+lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
+  unfolding Alm_all_def by simp
+
+lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
+  by (erule contrapos_pp, simp)
 
 lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
-  by (simp add: MOST_iff_finiteNeg)
+  by simp
+
+lemma INFM_E: assumes "INFM x. P x" obtains x where "P x"
+  using INFM_EX [OF assms] by (rule exE)
+
+lemma MOST_I: assumes "\<And>x. P x" shows "MOST x. P x"
+  using assms by simp
 
 lemma INFM_mono:
   assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
@@ -404,30 +421,95 @@
   "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
   unfolding Inf_many_def by (simp add: Collect_disj_eq)
 
+lemma INFM_imp_distrib:
+  "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
+  by (simp only: imp_conv_disj INFM_disj_distrib not_MOST)
+
 lemma MOST_conj_distrib:
   "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
   unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
 
+lemma MOST_conjI:
+  "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
+  by (simp add: MOST_conj_distrib)
+
+lemma INFM_conjI:
+  "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
+  unfolding MOST_iff_cofinite INFM_iff_infinite
+  apply (drule (1) Diff_infinite_finite)
+  apply (simp add: Collect_conj_eq Collect_neg_eq)
+  done
+
 lemma MOST_rev_mp:
   assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
   shows "\<forall>\<^sub>\<infinity>x. Q x"
 proof -
   have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
-    using prems by (simp add: MOST_conj_distrib)
+    using assms by (rule MOST_conjI)
   thus ?thesis by (rule MOST_mono) simp
 qed
 
-lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
-unfolding Alm_all_def not_not ..
+lemma MOST_imp_iff:
+  assumes "MOST x. P x"
+  shows "(MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
+proof
+  assume "MOST x. P x \<longrightarrow> Q x"
+  with assms show "MOST x. Q x" by (rule MOST_rev_mp)
+next
+  assume "MOST x. Q x"
+  then show "MOST x. P x \<longrightarrow> Q x" by (rule MOST_mono) simp
+qed
 
-lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
-unfolding Alm_all_def not_not ..
+lemma INFM_MOST_simps [simp]:
+  "\<And>P Q. (INFM x. P x \<and> Q) \<longleftrightarrow> (INFM x. P x) \<and> Q"
+  "\<And>P Q. (INFM x. P \<and> Q x) \<longleftrightarrow> P \<and> (INFM x. Q x)"
+  "\<And>P Q. (MOST x. P x \<or> Q) \<longleftrightarrow> (MOST x. P x) \<or> Q"
+  "\<And>P Q. (MOST x. P \<or> Q x) \<longleftrightarrow> P \<or> (MOST x. Q x)"
+  "\<And>P Q. (MOST x. P x \<longrightarrow> Q) \<longleftrightarrow> ((INFM x. P x) \<longrightarrow> Q)"
+  "\<And>P Q. (MOST x. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (MOST x. Q x))"
+  unfolding Alm_all_def Inf_many_def
+  by (simp_all add: Collect_conj_eq)
+
+text {* Properties of quantifiers with injective functions. *}
+
+lemma INFM_inj:
+  "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
+  unfolding INFM_iff_infinite
+  by (clarify, drule (1) finite_vimageI, simp)
 
-lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
-  unfolding Inf_many_def by simp
+lemma MOST_inj:
+  "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
+  unfolding MOST_iff_cofinite
+  by (drule (1) finite_vimageI, simp)
+
+text {* Properties of quantifiers with singletons. *}
+
+lemma not_INFM_eq [simp]:
+  "\<not> (INFM x. x = a)"
+  "\<not> (INFM x. a = x)"
+  unfolding INFM_iff_infinite by simp_all
+
+lemma MOST_neq [simp]:
+  "MOST x. x \<noteq> a"
+  "MOST x. a \<noteq> x"
+  unfolding MOST_iff_cofinite by simp_all
 
-lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
-  unfolding Alm_all_def by simp
+lemma INFM_neq [simp]:
+  "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
+  "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
+  unfolding INFM_iff_infinite by simp_all
+
+lemma MOST_eq [simp]:
+  "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
+  "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
+  unfolding MOST_iff_cofinite by simp_all
+
+lemma MOST_eq_imp:
+  "MOST x. x = a \<longrightarrow> P x"
+  "MOST x. a = x \<longrightarrow> P x"
+  unfolding MOST_iff_cofinite by simp_all
+
+text {* Properties of quantifiers over the naturals. *}
 
 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)"
   by (simp add: Inf_many_def infinite_nat_iff_unbounded)
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Fri Dec 18 12:00:29 2009 +0100
+++ b/src/HOL/Library/Product_Vector.thy	Fri Dec 18 12:00:44 2009 +0100
@@ -102,6 +102,42 @@
     by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
 qed
 
+lemma openI: (* TODO: move *)
+  assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"
+  shows "open S"
+proof -
+  have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto
+  moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms)
+  ultimately show "open S" by simp
+qed
+
+lemma subset_fst_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> y \<in> B \<Longrightarrow> A \<subseteq> fst ` S"
+  unfolding image_def subset_eq by force
+
+lemma subset_snd_imageI: "A \<times> B \<subseteq> S \<Longrightarrow> x \<in> A \<Longrightarrow> B \<subseteq> snd ` S"
+  unfolding image_def subset_eq by force
+
+lemma open_image_fst: assumes "open S" shows "open (fst ` S)"
+proof (rule openI)
+  fix x assume "x \<in> fst ` S"
+  then obtain y where "(x, y) \<in> S" by auto
+  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
+    using `open S` unfolding open_prod_def by auto
+  from `A \<times> B \<subseteq> S` `y \<in> B` have "A \<subseteq> fst ` S" by (rule subset_fst_imageI)
+  with `open A` `x \<in> A` have "open A \<and> x \<in> A \<and> A \<subseteq> fst ` S" by simp
+  then show "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> fst ` S" by - (rule exI)
+qed
+
+lemma open_image_snd: assumes "open S" shows "open (snd ` S)"
+proof (rule openI)
+  fix y assume "y \<in> snd ` S"
+  then obtain x where "(x, y) \<in> S" by auto
+  then obtain A B where "open A" "open B" "x \<in> A" "y \<in> B" "A \<times> B \<subseteq> S"
+    using `open S` unfolding open_prod_def by auto
+  from `A \<times> B \<subseteq> S` `x \<in> A` have "B \<subseteq> snd ` S" by (rule subset_snd_imageI)
+  with `open B` `y \<in> B` have "open B \<and> y \<in> B \<and> B \<subseteq> snd ` S" by simp
+  then show "\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> snd ` S" by - (rule exI)
+qed
 
 subsection {* Product is a metric space *}
 
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Dec 18 12:00:29 2009 +0100
+++ b/src/Pure/General/symbol.ML	Fri Dec 18 12:00:44 2009 +0100
@@ -34,6 +34,7 @@
   val is_ascii_hex: symbol -> bool
   val is_ascii_quasi: symbol -> bool
   val is_ascii_blank: symbol -> bool
+  val is_ascii_control: symbol -> bool
   val is_ascii_lower: symbol -> bool
   val is_ascii_upper: symbol -> bool
   val to_ascii_lower: symbol -> symbol
@@ -163,6 +164,8 @@
   fn " " => true | "\t" => true | "\n" => true | "\^K" => true | "\^L" => true | "\^M" => true
     | _ => false;
 
+fun is_ascii_control s = is_char s andalso ord s < 32 andalso not (is_ascii_blank s);
+
 fun is_ascii_lower s = is_char s andalso (ord "a" <= ord s andalso ord s <= ord "z");
 fun is_ascii_upper s = is_char s andalso (ord "A" <= ord s andalso ord s <= ord "Z");
 
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Fri Dec 18 12:00:29 2009 +0100
+++ b/src/Pure/General/symbol.scala	Fri Dec 18 12:00:44 2009 +0100
@@ -214,7 +214,7 @@
        new Recoder(mapping map { case (x, y) => (y, x) }))
     }
 
-    def decode(text: String) = decoder.recode(text)
-    def encode(text: String) = encoder.recode(text)
+    def decode(text: String): String = decoder.recode(text)
+    def encode(text: String): String = encoder.recode(text)
   }
 }
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Fri Dec 18 12:00:29 2009 +0100
+++ b/src/Pure/General/xml.scala	Fri Dec 18 12:00:44 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] =
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Fri Dec 18 12:00:29 2009 +0100
+++ b/src/Pure/General/yxml.ML	Fri Dec 18 12:00:44 2009 +0100
@@ -15,6 +15,7 @@
 
 signature YXML =
 sig
+  val binary_text: string -> string
   val output_markup: Markup.T -> string * string
   val element: string -> XML.attributes -> string list -> string
   val string_of: XML.tree -> string
@@ -27,6 +28,19 @@
 
 (** string representation **)
 
+(* binary_text -- idempotent recoding *)
+
+fun pseudo_utf8 c =
+  if Symbol.is_ascii_control c
+  then chr 192 ^ chr (128 + ord c)
+  else c;
+
+fun binary_text str =
+  if exists_string Symbol.is_ascii_control str
+  then translate_string pseudo_utf8 str
+  else str;
+
+
 (* markers *)
 
 val X = Symbol.ENQ;
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Fri Dec 18 12:00:29 2009 +0100
+++ b/src/Pure/General/yxml.scala	Fri Dec 18 12:00:44 2009 +0100
@@ -19,7 +19,8 @@
 
   /* iterate over chunks (resembles space_explode in ML) */
 
-  private def chunks(sep: Char, source: CharSequence) = new Iterator[CharSequence] {
+  private def chunks(sep: Char, source: CharSequence) = new Iterator[CharSequence]
+  {
     private val end = source.length
     private var state = if (end == 0) None else get_chunk(-1)
     private def get_chunk(i: Int) =
@@ -39,6 +40,68 @@
   }
 
 
+  /* decoding pseudo UTF-8 */
+
+  private class Decode_Chars(decode: String => String,
+    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
+  {
+    def length: Int = end - start
+    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
+    def subSequence(i: Int, j: Int): CharSequence =
+      new Decode_Chars(decode, buffer, start + i, start + j)
+
+    // toString with adhoc decoding: abuse of CharSequence interface
+    // see also http://en.wikipedia.org/wiki/UTF-8#Description
+    override def toString: String =
+    {
+      val buf = new java.lang.StringBuilder(length)
+      var code = -1
+      var rest = 0
+      def flush()
+      {
+        if (code != -1) {
+          if (rest == 0) buf.appendCodePoint(code)
+          else buf.append('\uFFFD')
+          code = -1
+          rest = 0
+        }
+      }
+      def init(x: Int, n: Int)
+      {
+        flush()
+        code = x
+        rest = n
+      }
+      def push(x: Int)
+      {
+        if (rest <= 0) init(x, -1)
+        else {
+          code <<= 6
+          code += x
+          rest -= 1
+        }
+      }
+      for (i <- 0 until length) {
+        val c = charAt(i)
+        if (c < 128) { flush(); buf.append(c) }
+        else if ((c & 0xC0) == 0x80) push(c & 0x3F)
+        else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
+        else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2)
+        else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3)
+      }
+      flush()
+      decode(buf.toString)
+    }
+  }
+
+  def decode_chars(decode: String => String,
+    buffer: Array[Byte], start: Int, end: Int): CharSequence =
+  {
+    require(0 <= start && start <= end && end <= buffer.length)
+    new Decode_Chars(decode, buffer, start, end)
+  }
+
+
   /* parsing */
 
   private def err(msg: String) = error("Malformed YXML: " + msg)
@@ -80,11 +143,12 @@
     /* parse chunks */
 
     stack = List((("", Nil), Nil))
-    for (chunk <- chunks(X, source) if chunk != "") {
-      if (chunk == Y_string) pop()
+    for (chunk <- chunks(X, source) if chunk.length != 0) {
+      if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
       else {
         chunks(Y, chunk).toList match {
-          case "" :: name :: atts => push(name.toString.intern, atts.map(parse_attrib))
+          case ch :: name :: atts if ch.length == 0 =>
+            push(name.toString.intern, atts.map(parse_attrib))
           case txts => for (txt <- txts) add(XML.Text(txt.toString))
         }
       }
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/Pure/IsaMakefile
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Dec 18 12:00:29 2009 +0100
+++ b/src/Pure/System/isabelle_process.ML	Fri Dec 18 12:00:44 2009 +0100
@@ -1,24 +1,11 @@
 (*  Title:      Pure/System/isabelle_process.ML
     Author:     Makarius
 
-Isabelle process wrapper -- interaction via external program.
+Isabelle process wrapper.
 
 General format of process output:
-
-  (1) unmarked stdout/stderr, no line structure (output should be
-  processed immediately as it arrives);
-
-  (2) properly marked-up messages, e.g. for writeln channel
-
-  "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
-
-  where the props consist of name=value lines terminated by "\002,\n"
-  each, and the remaining text is any number of lines (output is
-  supposed to be processed in one piece);
-
-  (3) special init message holds "pid" and "session" property;
-
-  (4) message content is encoded in YXML format.
+  (1) message = "\002"  header chunk  body chunk
+  (2) chunk = size (ASCII digits)  \n  content (YXML)
 *)
 
 signature ISABELLE_PROCESS =
@@ -40,47 +27,28 @@
 
 (* message markup *)
 
-fun special ch = Symbol.STX ^ ch;
-val special_sep = special ",";
-val special_end = special ".";
-
 local
 
-fun clean_string bad str =
-  if exists_string (member (op =) bad) str then
-    translate_string (fn c => if member (op =) bad c then Symbol.DEL else c) str
-  else str;
+fun chunk s = string_of_int (size s) ^ "\n" ^ s;
 
-fun message_props props =
-  let val clean = clean_string [Symbol.STX, "\n", "\r"]
-  in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
-
-fun message_pos trees = trees |> get_first
-  (fn XML.Elem (name, atts, ts) =>
-        if name = Markup.positionN then SOME (Position.of_properties atts)
-        else message_pos ts
-    | _ => NONE);
+fun message _ _ _ "" = ()
+  | message out_stream ch props body =
+      let
+        val header = YXML.string_of (XML.Elem (ch, map (pairself YXML.binary_text) props, []));
+        val msg = Symbol.STX ^ chunk header ^ chunk body;
+      in TextIO.output (out_stream, msg) (*atomic output*) end;
 
 in
 
-fun message _ _ "" = ()
-  | message out_stream ch body =
-      let
-        val pos = the_default Position.none (message_pos (YXML.parse_body body));
-        val props =
-          Position.properties_of (Position.thread_data ())
-          |> Position.default_properties pos;
-        val txt = clean_string [Symbol.STX] body;
-        val msg = special ch ^ message_props props ^ txt ^ special_end ^ "\n";
-      in TextIO.output (out_stream, msg) end;
+fun standard_message out_stream ch body =
+  message out_stream ch (Position.properties_of (Position.thread_data ())) body;
 
 fun init_message out_stream =
   let
     val pid = (Markup.pidN, process_id ());
     val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
     val text = Session.welcome ();
-    val msg = special "A" ^ message_props [pid, session] ^ text ^ special_end ^ "\n";
-  in TextIO.output (out_stream, msg) end;
+  in message out_stream "A" [pid, session] text end;
 
 end;
 
@@ -100,25 +68,20 @@
 
 fun setup_channels out =
   let
-    val out_stream =
-      if out = "-" then TextIO.stdOut
-      else
-        let
-          val path = File.platform_path (Path.explode out);
-          val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
-          val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
-          val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
-        in out_stream end;
+    val path = File.platform_path (Path.explode out);
+    val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
+    val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
     val _ = SimpleThread.fork false (auto_flush out_stream);
+    val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
     val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
   in
-    Output.status_fn   := message out_stream "B";
-    Output.writeln_fn  := message out_stream "C";
-    Output.priority_fn := message out_stream "D";
-    Output.tracing_fn  := message out_stream "E";
-    Output.warning_fn  := message out_stream "F";
-    Output.error_fn    := message out_stream "G";
-    Output.debug_fn    := message out_stream "H";
+    Output.status_fn   := standard_message out_stream "B";
+    Output.writeln_fn  := standard_message out_stream "C";
+    Output.priority_fn := standard_message out_stream "D";
+    Output.tracing_fn  := standard_message out_stream "E";
+    Output.warning_fn  := standard_message out_stream "F";
+    Output.error_fn    := standard_message out_stream "G";
+    Output.debug_fn    := standard_message out_stream "H";
     Output.prompt_fn   := ignore;
     out_stream
   end;
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Fri Dec 18 12:00:29 2009 +0100
+++ b/src/Pure/System/isabelle_process.scala	Fri Dec 18 12:00:44 2009 +0100
@@ -82,12 +82,15 @@
       kind == STATUS
   }
 
-  class Result(val kind: Kind.Value, val props: List[(String, String)], val result: String) {
-    override def toString = {
-      val trees = YXML.parse_body_failsafe(result)
+  class Result(val kind: Kind.Value, val props: List[(String, String)], val body: List[XML.Tree])
+  {
+    def message = XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(kind)) :: props, body)
+
+    override def toString: String =
+    {
       val res =
-        if (kind == Kind.STATUS) trees.map(_.toString).mkString
-        else trees.flatMap(XML.content(_).mkString).mkString
+        if (kind == Kind.STATUS) body.map(_.toString).mkString
+        else body.map(XML.content(_).mkString).mkString
       if (props.isEmpty)
         kind.toString + " [[" + res + "]]"
       else
@@ -97,17 +100,14 @@
     def is_raw = Kind.is_raw(kind)
     def is_control = Kind.is_control(kind)
     def is_system = Kind.is_system(kind)
-  }
 
-  def parse_message(isabelle_system: Isabelle_System, result: Result) =
-  {
-    XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
-      YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
+    def cache(table: XML.Cache): Result =
+      new Result(kind, table.cache_props(props), table(body))
   }
 }
 
 
-class Isabelle_Process(isabelle_system: Isabelle_System, receiver: Actor, args: String*)
+class Isabelle_Process(system: Isabelle_System, receiver: Actor, args: String*)
 {
   import Isabelle_Process._
 
@@ -130,14 +130,19 @@
 
   /* results */
 
-  private def put_result(kind: Kind.Value, props: List[(String, String)], result: String)
+  private def put_result(kind: Kind.Value, props: List[(String, String)], body: List[XML.Tree])
   {
     if (kind == Kind.INIT) {
       val map = Map(props: _*)
       if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
       if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
     }
-    receiver ! new Result(kind, props, result)
+    receiver ! new Result(kind, props, body)
+  }
+
+  private def put_result(kind: Kind.Value, text: String)
+  {
+    put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
   }
 
 
@@ -145,13 +150,13 @@
 
   def interrupt() = synchronized {
     if (proc == null) error("Cannot interrupt Isabelle: no process")
-    if (pid == null) put_result(Kind.SYSTEM, Nil, "Cannot interrupt: unknown pid")
+    if (pid == null) put_result(Kind.SYSTEM, "Cannot interrupt: unknown pid")
     else {
       try {
-        if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
-          put_result(Kind.SIGNAL, Nil, "INT")
+        if (system.execute(true, "kill", "-INT", pid).waitFor == 0)
+          put_result(Kind.SIGNAL, "INT")
         else
-          put_result(Kind.SYSTEM, Nil, "Cannot interrupt: kill command failed")
+          put_result(Kind.SYSTEM, "Cannot interrupt: kill command failed")
       }
       catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
     }
@@ -162,7 +167,7 @@
     else {
       try_close()
       Thread.sleep(500)
-      put_result(Kind.SIGNAL, Nil, "KILL")
+      put_result(Kind.SIGNAL, "KILL")
       proc.destroy
       proc = null
       pid = null
@@ -222,17 +227,17 @@
             finished = true
           }
           else {
-            put_result(Kind.STDIN, Nil, s)
+            put_result(Kind.STDIN, s)
             writer.write(s)
             writer.flush
           }
           //}}}
         }
         catch {
-          case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdin thread: " + e.getMessage)
+          case e: IOException => put_result(Kind.SYSTEM, "Stdin thread: " + e.getMessage)
         }
       }
-      put_result(Kind.SYSTEM, Nil, "Stdin thread terminated")
+      put_result(Kind.SYSTEM, "Stdin thread terminated")
     }
   }
 
@@ -256,7 +261,7 @@
             else done = true
           }
           if (result.length > 0) {
-            put_result(Kind.STDOUT, Nil, result.toString)
+            put_result(Kind.STDOUT, result.toString)
             result.length = 0
           }
           else {
@@ -267,91 +272,89 @@
           //}}}
         }
         catch {
-          case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdout thread: " + e.getMessage)
+          case e: IOException => put_result(Kind.SYSTEM, "Stdout thread: " + e.getMessage)
         }
       }
-      put_result(Kind.SYSTEM, Nil, "Stdout thread terminated")
+      put_result(Kind.SYSTEM, "Stdout thread terminated")
     }
   }
 
 
   /* messages */
 
-  private class MessageThread(fifo: String) extends Thread("isabelle: messages") {
-    override def run() = {
-      val reader = isabelle_system.fifo_reader(fifo)
-      var kind: Kind.Value = null
-      var props: List[(String, String)] = Nil
-      var result = new StringBuilder
+  private class MessageThread(fifo: String) extends Thread("isabelle: messages")
+  {
+    private class Protocol_Error(msg: String) extends Exception(msg)
+    override def run()
+    {
+      val stream = system.fifo_stream(fifo)
+      val default_buffer = new Array[Byte](65536)
+      var c = -1
 
-      var finished = false
-      while (!finished) {
+      def read_chunk(): List[XML.Tree] =
+      {
+        //{{{
+        // chunk size
+        var n = 0
+        c = stream.read
+        while (48 <= c && c <= 57) {
+          n = 10 * n + (c - 48)
+          c = stream.read
+        }
+        if (c != 10) throw new Protocol_Error("bad message chunk header")
+
+        // chunk content
+        val buf =
+          if (n <= default_buffer.size) default_buffer
+          else new Array[Byte](n)
+
+        var i = 0
+        var m = 0
+        do {
+          m = stream.read(buf, i, n - i)
+          i += m
+        } while (m > 0 && n > i)
+
+        if (i != n) throw new Protocol_Error("bad message chunk content")
+
+        YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n))
+        //}}}
+      }
+
+      do {
         try {
-          if (kind == null) {
-            //{{{ Char mode -- resync
-            var c = -1
-            do {
-              c = reader.read
-              if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char])
-            } while (c >= 0 && c != 2)
-
-            if (result.length > 0) {
-              put_result(Kind.SYSTEM, Nil, "Malformed message:\n" + result.toString)
-              result.length = 0
-            }
-            if (c < 0) {
-              reader.close
-              finished = true
-              try_close()
-            }
-            else {
-              c = reader.read
-              if (Kind.code.isDefinedAt(c)) kind = Kind.code(c)
-              else kind = null
-            }
-            //}}}
+          //{{{
+          c = stream.read
+          var non_sync = 0
+          while (c >= 0 && c != 2) {
+            non_sync += 1
+            c = stream.read
           }
-          else {
-            //{{{ Line mode
-            val line = reader.readLine
-            if (line == null) {
-              reader.close
-              finished = true
-              try_close()
+          if (non_sync > 0)
+            throw new Protocol_Error("lost synchronization -- skipping " + non_sync + " bytes")
+          if (c == 2) {
+            val header = read_chunk()
+            val body = read_chunk()
+            header match {
+              case List(XML.Elem(name, props, Nil))
+                  if name.size == 1 && Kind.code.isDefinedAt(name(0)) =>
+                put_result(Kind.code(name(0)), props, body)
+              case _ => throw new Protocol_Error("bad header: " + header.toString)
             }
-            else {
-              val len = line.length
-              // property
-              if (line.endsWith("\u0002,")) {
-                val i = line.indexOf('=')
-                if (i > 0) {
-                  val name = line.substring(0, i)
-                  val value = line.substring(i + 1, len - 2)
-                  props = (name, value) :: props
-                }
-              }
-              // last text line
-              else if (line.endsWith("\u0002.")) {
-                result.append(line.substring(0, len - 2))
-                put_result(kind, props.reverse, result.toString)
-                kind = null
-                props = Nil
-                result.length = 0
-              }
-              // text line
-              else {
-                result.append(line)
-                result.append('\n')
-              }
-            }
-            //}}}
           }
+          //}}}
         }
         catch {
-          case e: IOException => put_result(Kind.SYSTEM, Nil, "Message thread: " + e.getMessage)
+          case e: IOException =>
+            put_result(Kind.SYSTEM, "Cannot read message:\n" + e.getMessage)
+          case e: Protocol_Error =>
+            put_result(Kind.SYSTEM, "Malformed message:\n" + e.getMessage)
         }
-      }
-      put_result(Kind.SYSTEM, Nil, "Message thread terminated")
+      } while (c != -1)
+      stream.close
+      try_close()
+
+      put_result(Kind.SYSTEM, "Message thread terminated")
     }
   }
 
@@ -363,16 +366,16 @@
     /* isabelle version */
 
     {
-      val (msg, rc) = isabelle_system.isabelle_tool("version")
+      val (msg, rc) = system.isabelle_tool("version")
       if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
-      put_result(Kind.SYSTEM, Nil, msg)
+      put_result(Kind.SYSTEM, msg)
     }
 
 
     /* messages */
 
-    val message_fifo = isabelle_system.mk_fifo()
-    def rm_fifo() = isabelle_system.rm_fifo(message_fifo)
+    val message_fifo = system.mk_fifo()
+    def rm_fifo() = system.rm_fifo(message_fifo)
 
     val message_thread = new MessageThread(message_fifo)
     message_thread.start
@@ -381,9 +384,8 @@
     /* exec process */
 
     try {
-      val cmdline =
-        List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
-      proc = isabelle_system.execute(true, cmdline: _*)
+      val cmdline = List(system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
+      proc = system.execute(true, cmdline: _*)
     }
     catch {
       case e: IOException =>
@@ -404,8 +406,8 @@
       override def run() = {
         val rc = proc.waitFor()
         Thread.sleep(300)
-        put_result(Kind.SYSTEM, Nil, "Exit thread terminated")
-        put_result(Kind.EXIT, Nil, Integer.toString(rc))
+        put_result(Kind.SYSTEM, "Exit thread terminated")
+        put_result(Kind.EXIT, rc.toString)
         rm_fifo()
       }
     }.start
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Dec 18 12:00:29 2009 +0100
+++ b/src/Pure/System/isabelle_system.scala	Fri Dec 18 12:00:44 2009 +0100
@@ -8,7 +8,7 @@
 
 import java.util.regex.Pattern
 import java.util.Locale
-import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException}
+import java.io.{BufferedInputStream, FileInputStream, File, IOException}
 import java.awt.{GraphicsEnvironment, Font}
 
 import scala.io.Source
@@ -279,13 +279,13 @@
     if (rc != 0) error(result)
   }
 
-  def fifo_reader(fifo: String): BufferedReader =
+  def fifo_stream(fifo: String): BufferedInputStream =
   {
     // blocks until writer is ready
     val stream =
       if (Platform.is_windows) execute(false, "cat", fifo).getInputStream
       else new FileInputStream(fifo)
-    new BufferedReader(new InputStreamReader(stream, Isabelle_System.charset))
+    new BufferedInputStream(stream)
   }
 
 
diff -r 8a2c5d7aff51 -r 85257fa296f6 src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Fri Dec 18 12:00:29 2009 +0100
+++ b/src/Pure/Thy/completion.scala	Fri Dec 18 12:00:44 2009 +0100
@@ -32,7 +32,7 @@
 
     override def toString: String =
     {
-      val buf = new StringBuffer(length)
+      val buf = new StringBuilder(length)
       for (i <- 0 until length)
         buf.append(charAt(i))
       buf.toString