--- 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)
--- 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)
--- 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 *}
--- 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");
--- 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)
}
}
--- 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] =
--- 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;
--- 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))
}
}
--- 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;
--- 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
--- 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)
}
--- 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