--- a/src/HOL/Finite_Set.thy Thu Dec 17 13:49:36 2009 -0800
+++ b/src/HOL/Finite_Set.thy Thu Dec 17 13:51:50 2009 -0800
@@ -2067,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)
@@ -2123,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/Pure/General/symbol.ML Thu Dec 17 13:49:36 2009 -0800
+++ b/src/Pure/General/symbol.ML Thu Dec 17 13:51:50 2009 -0800
@@ -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 Thu Dec 17 13:49:36 2009 -0800
+++ b/src/Pure/General/symbol.scala Thu Dec 17 13:51:50 2009 -0800
@@ -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/yxml.ML Thu Dec 17 13:49:36 2009 -0800
+++ b/src/Pure/General/yxml.ML Thu Dec 17 13:51:50 2009 -0800
@@ -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 Thu Dec 17 13:49:36 2009 -0800
+++ b/src/Pure/General/yxml.scala Thu Dec 17 13:51:50 2009 -0800
@@ -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 Thu Dec 17 13:49:36 2009 -0800
+++ b/src/Pure/System/isabelle_process.ML Thu Dec 17 13:51:50 2009 -0800
@@ -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 Thu Dec 17 13:49:36 2009 -0800
+++ b/src/Pure/System/isabelle_process.scala Thu Dec 17 13:51:50 2009 -0800
@@ -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
@@ -98,16 +101,10 @@
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)))
- }
}
-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 +127,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 +147,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 +164,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 +224,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 +258,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 +269,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 +363,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 +381,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 +403,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 Thu Dec 17 13:49:36 2009 -0800
+++ b/src/Pure/System/isabelle_system.scala Thu Dec 17 13:51:50 2009 -0800
@@ -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 Thu Dec 17 13:49:36 2009 -0800
+++ b/src/Pure/Thy/completion.scala Thu Dec 17 13:51:50 2009 -0800
@@ -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