# HG changeset patch # User wenzelm # Date 1261080777 -3600 # Node ID 9996f47a13109e735d66759a011937b7e2ab74fd # Parent a85e9c5b3cb79928e8951cf6b088749c4cd75d7e# Parent ea24958c2af517259171fa8e519475b864ba6af6 merged diff -r a85e9c5b3cb7 -r 9996f47a1310 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Thu Dec 17 17:05:56 2009 +0000 +++ b/src/Pure/General/symbol.ML Thu Dec 17 21:12:57 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 a85e9c5b3cb7 -r 9996f47a1310 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Thu Dec 17 17:05:56 2009 +0000 +++ b/src/Pure/General/symbol.scala Thu Dec 17 21:12:57 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 a85e9c5b3cb7 -r 9996f47a1310 src/Pure/General/yxml.ML --- a/src/Pure/General/yxml.ML Thu Dec 17 17:05:56 2009 +0000 +++ b/src/Pure/General/yxml.ML Thu Dec 17 21:12:57 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 a85e9c5b3cb7 -r 9996f47a1310 src/Pure/General/yxml.scala --- a/src/Pure/General/yxml.scala Thu Dec 17 17:05:56 2009 +0000 +++ b/src/Pure/General/yxml.scala Thu Dec 17 21:12:57 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 a85e9c5b3cb7 -r 9996f47a1310 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Thu Dec 17 17:05:56 2009 +0000 +++ b/src/Pure/System/isabelle_process.ML Thu Dec 17 21:12:57 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 a85e9c5b3cb7 -r 9996f47a1310 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Thu Dec 17 17:05:56 2009 +0000 +++ b/src/Pure/System/isabelle_process.scala Thu Dec 17 21:12:57 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 @@ -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 diff -r a85e9c5b3cb7 -r 9996f47a1310 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu Dec 17 17:05:56 2009 +0000 +++ b/src/Pure/System/isabelle_system.scala Thu Dec 17 21:12:57 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 a85e9c5b3cb7 -r 9996f47a1310 src/Pure/Thy/completion.scala --- a/src/Pure/Thy/completion.scala Thu Dec 17 17:05:56 2009 +0000 +++ b/src/Pure/Thy/completion.scala Thu Dec 17 21:12:57 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