# HG changeset patch # User wenzelm # Date 1262022013 -3600 # Node ID ff5486262cd6c56ea0bbfb64ba637a483f766bbb # Parent aecdcaaa8ff32529574ed417d9e169c2d7fe6f03 moved Library.decode_permissive_utf8 to Isabelle_System; moved Library.with_tmp_file to Isabelle_System; added Isabelle_System.read_file/write_file; added Isabelle_System.system_out, with propagation of thread interrupts and process shutdown (global CTRL-C); diff -r aecdcaaa8ff3 -r ff5486262cd6 src/Pure/General/yxml.scala --- a/src/Pure/General/yxml.scala Mon Dec 28 18:37:11 2009 +0100 +++ b/src/Pure/General/yxml.scala Mon Dec 28 18:40:13 2009 +0100 @@ -51,7 +51,7 @@ new Decode_Chars(decode, buffer, start + i, start + j) // toString with adhoc decoding: abuse of CharSequence interface - override def toString: String = decode(Library.decode_permissive_utf8(this)) + override def toString: String = decode(Isabelle_System.decode_permissive_utf8(this)) } def decode_chars(decode: String => String, diff -r aecdcaaa8ff3 -r ff5486262cd6 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Dec 28 18:37:11 2009 +0100 +++ b/src/Pure/System/isabelle_system.scala Mon Dec 28 18:40:13 2009 +0100 @@ -8,7 +8,8 @@ import java.util.regex.Pattern import java.util.Locale -import java.io.{BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader, +import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, + BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader, File, IOException} import java.awt.{GraphicsEnvironment, Font} @@ -22,6 +23,84 @@ val charset = "UTF-8" + /* permissive UTF-8 decoding */ + + // see also http://en.wikipedia.org/wiki/UTF-8#Description + def decode_permissive_utf8(text: CharSequence): String = + { + val buf = new java.lang.StringBuilder(text.length) + var code = -1 + var rest = 0 + def flush() + { + if (code != -1) { + if (rest == 0 && Character.isValidCodePoint(code)) + 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 text.length) { + val c = text.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() + buf.toString + } + + + /* basic file operations */ + + def with_tmp_file[A](prefix: String)(body: File => A): A = + { + val file = File.createTempFile(prefix, null) + val result = + try { body(file) } + finally { file.delete } + result + } + + def read_file(file: File): String = + { + val buf = new StringBuilder(file.length.toInt) + val reader = new BufferedReader(new InputStreamReader(new FileInputStream(file), charset)) + var c = reader.read + while (c != -1) { + buf.append(c.toChar) + c = reader.read + } + reader.close + buf.toString + } + + def write_file(file: File, text: CharSequence) + { + val writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset)) + try { writer.append(text) } + finally { writer.close } + } + + /* shell processes */ private def raw_execute(env: Map[String, String], redirect: Boolean, args: String*): Process = @@ -90,7 +169,7 @@ case Some(path) => path } - Library.with_tmp_file("isabelle_settings") { dump => + Isabelle_System.with_tmp_file("isabelle_settings") { dump => val cmdline = shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString) val (output, rc) = @@ -256,6 +335,62 @@ Isabelle_System.raw_execute(environment, redirect, cmdline: _*) } + def system_out(script: String): (String, Int) = + { + Isabelle_System.with_tmp_file("isabelle_script") { script_file => + Isabelle_System.with_tmp_file("isabelle_pid") { pid_file => + Isabelle_System.with_tmp_file("isabelle_output") { output_file => + + Isabelle_System.write_file(script_file, script) + + val proc = execute(true, "perl", "-w", + expand_path("$ISABELLE_HOME/lib/scripts/system.pl"), "group", + script_file.getPath, pid_file.getPath, output_file.getPath) + + def kill() = + { + val (pid, running0) = + try { (Isabelle_System.read_file(pid_file), true) } + catch { case _: IOException => ("", false) } + + var running = running0 + for (n <- 1 to 10 if running) { + if (execute(true, "kill", "-INT", "-" + pid).waitFor == 0) + Thread.sleep(100) + else running = false + } + } + + val shutdown_hook = new Thread { override def run = kill() } + Runtime.getRuntime.addShutdownHook(shutdown_hook) + + def cleanup() = + try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } + catch { case _: IllegalStateException => } + + val rc = + try { + try { proc.waitFor } // FIXME read stderr (!??) + catch { case e: InterruptedException => Thread.interrupted; kill(); throw e } + } + finally { + proc.getOutputStream.close + proc.getInputStream.close + proc.getErrorStream.close + proc.destroy + cleanup() + } + + val output = + try { Isabelle_System.read_file(output_file) } + catch { case _: IOException => "" } + + (output, rc) + } + } + } + } + def isabelle_tool(name: String, args: String*): (String, Int) = { getenv_strict("ISABELLE_TOOLS").split(":").find(dir => { diff -r aecdcaaa8ff3 -r ff5486262cd6 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Mon Dec 28 18:37:11 2009 +0100 +++ b/src/Pure/Thy/thy_header.scala Mon Dec 28 18:40:13 2009 +0100 @@ -36,8 +36,8 @@ val header: Parser[Header] = { - val file_name = atom("file name", _.is_name) ^^ Library.decode_permissive_utf8 - val theory_name = atom("theory name", _.is_name) ^^ Library.decode_permissive_utf8 + val file_name = atom("file name", _.is_name) ^^ Isabelle_System.decode_permissive_utf8 + val theory_name = atom("theory name", _.is_name) ^^ Isabelle_System.decode_permissive_utf8 val file = keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name diff -r aecdcaaa8ff3 -r ff5486262cd6 src/Pure/library.scala --- a/src/Pure/library.scala Mon Dec 28 18:37:11 2009 +0100 +++ b/src/Pure/library.scala Mon Dec 28 18:40:13 2009 +0100 @@ -7,7 +7,6 @@ package isabelle import java.lang.System -import java.io.File object Library @@ -37,64 +36,6 @@ } - /* permissive UTF-8 decoding */ - - // see also http://en.wikipedia.org/wiki/UTF-8#Description - def decode_permissive_utf8(text: CharSequence): String = - { - val buf = new java.lang.StringBuilder(text.length) - var code = -1 - var rest = 0 - def flush() - { - if (code != -1) { - if (rest == 0 && Character.isValidCodePoint(code)) - 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 text.length) { - val c = text.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() - buf.toString - } - - - /* temporary file */ - - def with_tmp_file[A](prefix: String)(body: File => A): A = - { - val file = File.createTempFile(prefix, null) - val result = - try { body(file) } - finally { file.delete } - result - } - - /* timing */ def timeit[A](e: => A) =