# HG changeset patch # User wenzelm # Date 1220034968 -7200 # Node ID 3533485fc7b8cb14671ceb7c3da376a89039c489 # Parent f454a20c1ab1c5d3125bf8c3968b0fb06e0e1a86 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo; IsabelleSystem.exec: varargs convenience; more robust message thread management: no interrupt, but proper rendezvous via fifo (rm_fifo removes unused fifo, if isabelle-process fails); diff -r f454a20c1ab1 -r 3533485fc7b8 lib/Tools/rmfifo --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/Tools/rmfifo Fri Aug 29 20:36:08 2008 +0200 @@ -0,0 +1,30 @@ +#!/usr/bin/env bash +# +# $Id$ +# Author: Makarius +# +# DESCRIPTION: remove named pipe + + +PRG="$(basename "$0")" + +function usage() +{ + echo + echo "Usage: $PRG NAME" + echo + echo " Remove an unused named pipe, after producing dummy output" + echo " to unblock the reader (blocks if no reader present)." + echo + exit 1 +} + + +## main + +[ "$#" != 1 ] && usage +FIFO="$1"; shift + +if [ -p "$FIFO" ]; then + echo -n "" >"$FIFO" && rm -f "$FIFO" +fi diff -r f454a20c1ab1 -r 3533485fc7b8 src/Pure/Tools/isabelle_process.scala --- a/src/Pure/Tools/isabelle_process.scala Fri Aug 29 20:36:07 2008 +0200 +++ b/src/Pure/Tools/isabelle_process.scala Fri Aug 29 20:36:08 2008 +0200 @@ -110,7 +110,7 @@ if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid") else { try { - if (IsabelleSystem.exec(List("kill", "-INT", pid)).waitFor == 0) + if (IsabelleSystem.exec("kill", "-INT", pid).waitFor == 0) put_result(Kind.SIGNAL, null, "INT") else put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed") @@ -249,85 +249,81 @@ var finished = false while (!finished) { try { - 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, null, "Malformed message:\n" + result.toString) - result.length = 0 - } - if (c < 0) { - reader.close - finished = true - try_close() - } - else { - reader.read match { - case 'A' => kind = Kind.WRITELN - case 'B' => kind = Kind.PRIORITY - case 'C' => kind = Kind.TRACING - case 'D' => kind = Kind.WARNING - case 'E' => kind = Kind.ERROR - case 'F' => kind = Kind.DEBUG - case 'G' => kind = Kind.PROMPT - case 'H' => kind = Kind.INIT - case 'I' => kind = Kind.STATUS - case _ => kind = null - } - props = null - } - //}}} + 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, null, "Malformed message:\n" + result.toString) + result.length = 0 + } + if (c < 0) { + reader.close + finished = true + try_close() } else { - //{{{ Line mode - val line = reader.readLine - if (line == null) { - reader.close - finished = true - try_close() + reader.read match { + case 'A' => kind = Kind.WRITELN + case 'B' => kind = Kind.PRIORITY + case 'C' => kind = Kind.TRACING + case 'D' => kind = Kind.WARNING + case 'E' => kind = Kind.ERROR + case 'F' => kind = Kind.DEBUG + case 'G' => kind = Kind.PROMPT + case 'H' => kind = Kind.INIT + case 'I' => kind = Kind.STATUS + case _ => kind = null } - 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) - if (props == null) props = new Properties - if (!props.containsKey(name)) props.setProperty(name, value) - } - } - // last text line - else if (line.endsWith("\u0002.")) { - result.append(line.substring(0, len - 2)) - put_result(kind, props, result.toString) - result.length = 0 - kind = null - } - // text line - else { - result.append(line) - result.append('\n') + props = null + } + //}}} + } + else { + //{{{ Line mode + val line = reader.readLine + if (line == null) { + reader.close + finished = true + try_close() + } + 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) + if (props == null) props = new Properties + if (!props.containsKey(name)) props.setProperty(name, value) } } - //}}} + // last text line + else if (line.endsWith("\u0002.")) { + result.append(line.substring(0, len - 2)) + put_result(kind, props, result.toString) + result.length = 0 + kind = null + } + // text line + else { + result.append(line) + result.append('\n') + } } - } - catch { - case e: IOException => put_result(Kind.SYSTEM, null, "Message thread: " + e.getMessage) + //}}} } } - catch { case _: InterruptedException => finished = true } + catch { + case e: IOException => put_result(Kind.SYSTEM, null, "Message thread: " + e.getMessage) + } } - try { put_result(Kind.SYSTEM, null, "Message thread terminated") } - catch { case _ : InterruptedException => } + put_result(Kind.SYSTEM, null, "Message thread terminated") } } @@ -338,29 +334,24 @@ /* message fifo */ - val fifo = - try { - val mkfifo = IsabelleSystem.exec(List(IsabelleSystem.getenv_strict("ISATOOL"), "mkfifo")) - val fifo = new BufferedReader(new - InputStreamReader(mkfifo.getInputStream, IsabelleSystem.charset)).readLine - if (mkfifo.waitFor == 0) fifo - else error("Failed to create message fifo") - } - catch { - case e: IOException => error("Failed to create message fifo: " + e.getMessage) - } + val message_fifo = IsabelleSystem.mk_fifo() + def rm_fifo() = IsabelleSystem.rm_fifo(message_fifo) - val message_thread = new MessageThread(fifo) + val message_thread = new MessageThread(message_fifo) + message_thread.start /* exec process */ try { - proc = IsabelleSystem.exec2(List( - IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W", fifo) ++ args) + val cmdline = List(IsabelleSystem.getenv_strict("ISABELLE_HOME") + + "/bin/isabelle-process", "-W", message_fifo) ++ args + proc = IsabelleSystem.exec2(cmdline: _*) } catch { - case e: IOException => error("Failed to execute Isabelle process: " + e.getMessage) + case e: IOException => + rm_fifo() + error("Failed to execute Isabelle process: " + e.getMessage) } @@ -372,17 +363,16 @@ /* exit */ - class ExitThread extends Thread("isabelle: exit") { + new Thread("isabelle: exit") { override def run() = { val rc = proc.waitFor() Thread.sleep(300) put_result(Kind.SYSTEM, null, "Exit thread terminated") put_result(Kind.EXIT, null, Integer.toString(rc)) - message_thread.interrupt + rm_fifo() } - } - message_thread.start - new ExitThread().start + }.start + } } diff -r f454a20c1ab1 -r 3533485fc7b8 src/Pure/Tools/isabelle_system.scala --- a/src/Pure/Tools/isabelle_system.scala Fri Aug 29 20:36:07 2008 +0200 +++ b/src/Pure/Tools/isabelle_system.scala Fri Aug 29 20:36:08 2008 +0200 @@ -8,7 +8,9 @@ package isabelle import java.util.regex.{Pattern, Matcher} -import java.io.{BufferedReader, InputStreamReader, FileInputStream, File} +import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException} + +import scala.io.Source object IsabelleSystem { @@ -74,24 +76,48 @@ } - /* named pipes */ - - def fifo_reader(fifo: String) = - if (is_cygwin()) new BufferedReader(new InputStreamReader(Runtime.getRuntime.exec( - Array(platform_path("/bin/cat"), fifo)).getInputStream, charset)) - else new BufferedReader(new InputStreamReader(new FileInputStream(fifo), charset)) - - /* processes */ private def posix_prefix() = if (is_cygwin()) List(platform_path("/bin/env")) else Nil - def exec(args: List[String]) = Runtime.getRuntime.exec((posix_prefix() ++ args).toArray) + def exec(args: String*): Process = Runtime.getRuntime.exec((posix_prefix() ++ args).toArray) - def exec2(args: List[String]) = { + def exec2(args: String*): Process = { val cmdline = new java.util.LinkedList[String] for (s <- posix_prefix() ++ args) cmdline.add(s) new ProcessBuilder(cmdline).redirectErrorStream(true).start } + + /* Isabelle tools (non-interactive) */ + + def isatool(args: String*) = { + val proc = + try { exec2((List(getenv_strict("ISATOOL")) ++ args): _*) } + catch { case e: IOException => error(e.getMessage) } + proc.getOutputStream.close + val output = Source.fromInputStream(proc.getInputStream, charset).mkString("") + val rc = proc.waitFor + (output, rc) + } + + + /* named pipes */ + + def mk_fifo() = { + val (result, rc) = isatool("mkfifo") + if (rc == 0) result.trim + else error(result) + } + + def rm_fifo(fifo: String) = { + val (result, rc) = isatool("rmfifo", fifo) + if (rc != 0) error(result) + } + + def fifo_reader(fifo: String) = // blocks until writer is ready + if (is_cygwin()) new BufferedReader(new InputStreamReader(Runtime.getRuntime.exec( + Array(platform_path("/bin/cat"), fifo)).getInputStream, charset)) + else new BufferedReader(new InputStreamReader(new FileInputStream(fifo), charset)) + }