--- a/lib/scripts/bash Wed Sep 22 11:46:28 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Makarius
-#
-# bash - invoke shell command line (with robust signal handling)
-#
-
-use warnings;
-use strict;
-
-
-# args
-
-my ($group, $script_name, $pid_name, $output_name) = @ARGV;
-
-
-# process id
-
-if ($group eq "group") {
- use POSIX "setsid";
- POSIX::setsid || die $!;
-}
-
-open (PID_FILE, ">", $pid_name) || die $!;
-print PID_FILE "$$";
-close PID_FILE;
-
-
-# exec script
-
-exec qq/exec bash '$script_name' > '$output_name'/;
--- a/lib/scripts/feeder.pl Wed Sep 22 11:46:28 2010 +0200
+++ b/lib/scripts/feeder.pl Wed Sep 22 16:24:41 2010 +0200
@@ -27,9 +27,9 @@
$head && (print "$head", "\n");
if (!$quit) {
- while (<STDIN>) {
- print;
- }
+ while (<STDIN>) {
+ print;
+ }
}
$tail && (print "$tail", "\n");
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/process Wed Sep 22 16:24:41 2010 +0200
@@ -0,0 +1,46 @@
+#!/usr/bin/env perl
+#
+# Author: Makarius
+#
+# exec process - with optional process group and report of pid
+#
+
+use warnings;
+use strict;
+
+# process group
+
+my $group = $ARGV[0]; shift(@ARGV);
+
+if ($group eq "group") {
+ use POSIX "setsid";
+ POSIX::setsid || die $!;
+}
+
+
+# report pid
+
+my $pid_name = $ARGV[0]; shift(@ARGV);
+
+if ($pid_name eq "-") {
+ print "$$\n";
+}
+else {
+ open (PID_FILE, ">", $pid_name) || die $!;
+ print PID_FILE "$$";
+ close PID_FILE;
+}
+
+
+# exec process
+
+my $script = $ARGV[0]; shift(@ARGV);
+
+if ($script eq "script") {
+ my $cmd_line = $ARGV[0]; shift(@ARGV);
+ exec $cmd_line || die $!;
+}
+else {
+ (exec { $ARGV[0] } @ARGV) || die $!;
+}
+
--- a/src/Pure/Concurrent/simple_thread.scala Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala Wed Sep 22 16:24:41 2010 +0200
@@ -16,22 +16,34 @@
{
/* plain thread */
- def fork(name: String, daemon: Boolean = false)(body: => Unit): Thread =
+ def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
{
- val thread = new Thread(name) { override def run = body }
+ val thread =
+ if (name == null || name == "") new Thread() { override def run = body }
+ else new Thread(name) { override def run = body }
thread.setDaemon(daemon)
thread.start
thread
}
+ /* future result via thread */
+
+ def future[A](name: String = "", daemon: Boolean = false)(body: => A): Future[A] =
+ {
+ val result = Future.promise[A]
+ fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
+ result
+ }
+
+
/* thread as actor */
- def actor(name: String, daemon: Boolean = false)(body: => Unit): Actor =
+ def actor(name: String, daemon: Boolean = false)(body: => Unit): (Thread, Actor) =
{
val actor = Future.promise[Actor]
val thread = fork(name, daemon) { actor.fulfill(Actor.self); body }
- actor.join
+ (thread, actor.join)
}
}
--- a/src/Pure/General/markup.ML Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Pure/General/markup.ML Wed Sep 22 16:24:41 2010 +0200
@@ -114,7 +114,6 @@
val execN: string
val assignN: string val assign: int -> T
val editN: string val edit: int -> int -> T
- val pidN: string
val serialN: string
val promptN: string val prompt: T
val readyN: string val ready: T
@@ -340,7 +339,6 @@
(* messages *)
-val pidN = "pid";
val serialN = "serial";
val (promptN, prompt) = markup_elem "prompt";
--- a/src/Pure/General/markup.scala Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Pure/General/markup.scala Wed Sep 22 16:24:41 2010 +0200
@@ -227,7 +227,6 @@
/* messages */
- val PID = "pid"
val Serial = new Long_Property("serial")
val MESSAGE = "message"
@@ -248,7 +247,7 @@
val BAD = "bad"
- val Ready = Markup("ready", Nil)
+ val READY = "ready"
/* system data */
--- a/src/Pure/ML-Systems/bash.ML Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Pure/ML-Systems/bash.ML Wed Sep 22 16:24:41 2010 +0200
@@ -25,8 +25,8 @@
val output_name = OS.FileSys.tmpName ();
val status =
- OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" nogroup " ^
- script_name ^ " /dev/null " ^ output_name);
+ OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" no_group /dev/null" ^
+ " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
val rc =
(case Posix.Process.fromStatus status of
Posix.Process.W_EXITED => 0
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Wed Sep 22 16:24:41 2010 +0200
@@ -180,8 +180,8 @@
val system_thread = Thread.fork (fn () =>
let
val status =
- OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" group " ^
- script_name ^ " " ^ pid_name ^ " " ^ output_name);
+ OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^
+ " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\"");
val res =
(case Posix.Process.fromStatus status of
Posix.Process.W_EXITED => Result 0
--- a/src/Pure/ML-Systems/polyml_common.ML Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML Wed Sep 22 16:24:41 2010 +0200
@@ -111,9 +111,6 @@
val cd = OS.FileSys.chDir;
val pwd = OS.FileSys.getDir;
-fun process_id () =
- Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));
-
(* getenv *)
--- a/src/Pure/ML-Systems/smlnj.ML Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Wed Sep 22 16:24:41 2010 +0200
@@ -172,9 +172,6 @@
val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
-fun process_id pid =
- Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));
-
(* getenv *)
--- a/src/Pure/System/isabelle_process.ML Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed Sep 22 16:24:41 2010 +0200
@@ -78,7 +78,7 @@
(Position.properties_of (Position.thread_data ()))) body;
fun init_message out_stream =
- message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
+ message out_stream "A" [] (Session.welcome ());
end;
@@ -182,7 +182,7 @@
val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
val _ = init_message out_stream;
val _ = Keyword.status ();
- val _ = Output.status (Markup.markup Markup.ready "");
+ val _ = Output.status (Markup.markup Markup.ready "Prover ready");
in loop in_stream end));
end;
--- a/src/Pure/System/isabelle_process.scala Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala Wed Sep 22 16:24:41 2010 +0200
@@ -13,6 +13,7 @@
import scala.actors.Actor
import Actor._
+import scala.collection.mutable
object Isabelle_Process
@@ -43,7 +44,11 @@
def is_system = kind == Markup.SYSTEM
def is_status = kind == Markup.STATUS
def is_report = kind == Markup.REPORT
- def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
+ def is_ready = is_status && {
+ body match {
+ case List(XML.Elem(Markup(Markup.READY, _), _)) => true
+ case _ => false
+ }}
override def toString: String =
{
@@ -72,104 +77,26 @@
actor { loop { react { case res => Console.println(res) } } }, args: _*)
- /* input actors */
-
- private case class Input_Text(text: String)
- private case class Input_Chunks(chunks: List[Array[Byte]])
-
- private case object Close
- private def close(a: Actor) { if (a != null) a ! Close }
-
- @volatile private var standard_input: Actor = null
- @volatile private var command_input: Actor = null
-
-
- /* process manager */
-
- private val in_fifo = system.mk_fifo()
- private val out_fifo = system.mk_fifo()
- private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
+ /* system log */
- private val proc =
- try {
- val cmdline =
- List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
- system.execute(true, cmdline: _*)
- }
- catch { case e: IOException => rm_fifos(); throw(e) }
-
- private val stdout_reader =
- new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
-
- private val stdin_writer =
- new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
-
- Simple_Thread.actor("process_manager") {
- val (startup_failed, startup_output) =
- {
- val expired = System.currentTimeMillis() + timeout
- val result = new StringBuilder(100)
+ private val system_results = new mutable.ListBuffer[String]
- var finished = false
- while (!finished && System.currentTimeMillis() <= expired) {
- while (!finished && stdout_reader.ready) {
- val c = stdout_reader.read
- if (c == 2) finished = true
- else result += c.toChar
- }
- Thread.sleep(10)
- }
- (!finished, result.toString)
- }
- if (startup_failed) {
- put_result(Markup.STDOUT, startup_output)
- put_result(Markup.EXIT, "127")
- stdin_writer.close
- Thread.sleep(300) // FIXME !?
- proc.destroy // FIXME reliable!?
- }
- else {
- put_result(Markup.SYSTEM, startup_output)
+ private def system_result(text: String)
+ {
+ synchronized { system_results += text }
+ receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
+ }
- standard_input = stdin_actor()
- stdout_actor()
-
- // rendezvous
- val command_stream = system.fifo_output_stream(in_fifo)
- val message_stream = system.fifo_input_stream(out_fifo)
-
- command_input = input_actor(command_stream)
- message_actor(message_stream)
-
- val rc = proc.waitFor()
- Thread.sleep(300) // FIXME !?
- system_result("Isabelle process terminated")
- put_result(Markup.EXIT, rc.toString)
- }
- rm_fifos()
- }
+ def syslog(): List[String] = synchronized { system_results.toList }
/* results */
- private def system_result(text: String)
- {
- receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
- }
-
-
private val xml_cache = new XML.Cache(131071)
private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
{
- if (pid.isEmpty && kind == Markup.INIT) {
- rm_fifos()
- props.find(_._1 == Markup.PID).map(_._1) match {
- case None => system_result("Bad Isabelle process initialization: missing pid")
- case p => pid = p
- }
- }
-
+ if (kind == Markup.INIT) rm_fifos()
val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
xml_cache.cache_tree(msg)((message: XML.Tree) =>
receiver ! new Result(message.asInstanceOf[XML.Elem]))
@@ -181,36 +108,110 @@
}
- /* signals */
+ /* input actors */
+
+ private case class Input_Text(text: String)
+ private case class Input_Chunks(chunks: List[Array[Byte]])
+
+ private case object Close
+ private def close(p: (Thread, Actor))
+ {
+ if (p != null && p._1.isAlive) {
+ p._2 ! Close
+ p._1.join
+ }
+ }
+
+ @volatile private var standard_input: (Thread, Actor) = null
+ @volatile private var command_input: (Thread, Actor) = null
+
+
+ /** process manager **/
+
+ private val in_fifo = system.mk_fifo()
+ private val out_fifo = system.mk_fifo()
+ private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
+
+ private val process =
+ try {
+ val cmdline =
+ List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
+ new system.Managed_Process(true, cmdline: _*)
+ }
+ catch { case e: IOException => rm_fifos(); throw(e) }
+
+ val process_result =
+ Simple_Thread.future("process_result") { process.join }
+
+ private def terminate_process()
+ {
+ try { process.terminate }
+ catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) }
+ }
- @volatile private var pid: Option[String] = None
+ private val process_manager = Simple_Thread.fork("process_manager")
+ {
+ val (startup_failed, startup_output) =
+ {
+ val expired = System.currentTimeMillis() + timeout
+ val result = new StringBuilder(100)
+
+ var finished: Option[Boolean] = None
+ while (finished.isEmpty && System.currentTimeMillis() <= expired) {
+ while (finished.isEmpty && process.stdout.ready) {
+ val c = process.stdout.read
+ if (c == 2) finished = Some(true)
+ else result += c.toChar
+ }
+ if (process_result.is_finished) finished = Some(false)
+ else Thread.sleep(10)
+ }
+ (finished.isEmpty || !finished.get, result.toString)
+ }
+ system_result(startup_output)
+
+ if (startup_failed) {
+ put_result(Markup.EXIT, "127")
+ process.stdin.close
+ Thread.sleep(300)
+ terminate_process()
+ process_result.join
+ }
+ else {
+ // rendezvous
+ val command_stream = system.fifo_output_stream(in_fifo)
+ val message_stream = system.fifo_input_stream(out_fifo)
+
+ standard_input = stdin_actor()
+ val stdout = stdout_actor()
+ command_input = input_actor(command_stream)
+ val message = message_actor(message_stream)
+
+ val rc = process_result.join
+ system_result("Isabelle process terminated")
+ for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join
+ system_result("process_manager terminated")
+ put_result(Markup.EXIT, rc.toString)
+ }
+ rm_fifos()
+ }
+
+
+ /* management methods */
+
+ def join() { process_manager.join() }
def interrupt()
{
- pid match {
- case None => system_result("Cannot interrupt Isabelle: unknowd pid")
- case Some(i) =>
- try {
- if (system.execute(true, "kill", "-INT", i).waitFor == 0)
- system_result("Interrupt Isabelle")
- else
- system_result("Cannot interrupt Isabelle: kill command failed")
- }
- catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
- }
+ try { process.interrupt }
+ catch { case e: IOException => system_result("Failed to interrupt Isabelle: " + e.getMessage) }
}
- def kill()
+ def terminate()
{
- val running =
- try { proc.exitValue; false }
- catch { case e: java.lang.IllegalThreadStateException => true }
- if (running) {
- close()
- Thread.sleep(500) // FIXME !?
- system_result("Kill Isabelle")
- proc.destroy
- }
+ close()
+ system_result("Terminating Isabelle process")
+ terminate_process()
}
@@ -219,7 +220,7 @@
/* raw stdin */
- private def stdin_actor(): Actor =
+ private def stdin_actor(): (Thread, Actor) =
{
val name = "standard_input"
Simple_Thread.actor(name) {
@@ -229,10 +230,10 @@
//{{{
receive {
case Input_Text(text) =>
- stdin_writer.write(text)
- stdin_writer.flush
+ process.stdin.write(text)
+ process.stdin.flush
case Close =>
- stdin_writer.close
+ process.stdin.close
finished = true
case bad => System.err.println(name + ": ignoring bad message " + bad)
}
@@ -247,7 +248,7 @@
/* raw stdout */
- private def stdout_actor(): Actor =
+ private def stdout_actor(): (Thread, Actor) =
{
val name = "standard_output"
Simple_Thread.actor(name) {
@@ -259,8 +260,8 @@
//{{{
var c = -1
var done = false
- while (!done && (result.length == 0 || stdout_reader.ready)) {
- c = stdout_reader.read
+ while (!done && (result.length == 0 || process.stdout.ready)) {
+ c = process.stdout.read
if (c >= 0) result.append(c.asInstanceOf[Char])
else done = true
}
@@ -269,7 +270,7 @@
result.length = 0
}
else {
- stdout_reader.close
+ process.stdout.close
finished = true
}
//}}}
@@ -283,7 +284,7 @@
/* command input */
- private def input_actor(raw_stream: OutputStream): Actor =
+ private def input_actor(raw_stream: OutputStream): (Thread, Actor) =
{
val name = "command_input"
Simple_Thread.actor(name) {
@@ -314,7 +315,7 @@
/* message output */
- private def message_actor(stream: InputStream): Actor =
+ private def message_actor(stream: InputStream): (Thread, Actor) =
{
class EOF extends Exception
class Protocol_Error(msg: String) extends Exception(msg)
@@ -381,10 +382,10 @@
/** main methods **/
- def input_raw(text: String): Unit = standard_input ! Input_Text(text)
+ def input_raw(text: String): Unit = standard_input._2 ! Input_Text(text)
def input_bytes(name: String, args: Array[Byte]*): Unit =
- command_input ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
+ command_input._2 ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
def input(name: String, args: String*): Unit =
input_bytes(name, args.map(Standard_System.string_bytes): _*)
--- a/src/Pure/System/isabelle_system.scala Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Sep 22 16:24:41 2010 +0200
@@ -8,7 +8,8 @@
import java.util.regex.Pattern
import java.util.Locale
-import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File, IOException}
+import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File,
+ BufferedReader, InputStreamReader, BufferedWriter, OutputStreamWriter, IOException}
import java.awt.{GraphicsEnvironment, Font}
import java.awt.font.TextAttribute
@@ -70,17 +71,6 @@
}
- /* external processes */
-
- def execute(redirect: Boolean, args: String*): Process =
- {
- val cmdline =
- if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
- else args
- Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
- }
-
-
/* getenv */
def getenv(name: String): String =
@@ -194,68 +184,108 @@
- /** system tools **/
+ /** external processes **/
+
+ /* plain execute */
+
+ def execute(redirect: Boolean, args: String*): Process =
+ {
+ val cmdline =
+ if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
+ else args
+ Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
+ }
+
+
+ /* managed process */
+
+ class Managed_Process(redirect: Boolean, args: String*)
+ {
+ private val params =
+ List(expand_path("$ISABELLE_HOME/lib/scripts/process"), "group", "-", "no_script")
+ private val proc = execute(redirect, (params ++ args):_*)
+
+
+ // channels
+
+ val stdin: BufferedWriter =
+ new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
+
+ val stdout: BufferedReader =
+ new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
+
+ val stderr: BufferedReader =
+ new BufferedReader(new InputStreamReader(proc.getErrorStream, Standard_System.charset))
+
+
+ // signals
+
+ private val pid = stdout.readLine
- def bash_output(script: String): (String, Int) =
+ private def kill(signal: String): Boolean =
+ {
+ execute(true, "kill", "-" + signal, "-" + pid).waitFor
+ execute(true, "kill", "-0", "-" + pid).waitFor == 0
+ }
+
+ private def multi_kill(signal: String): Boolean =
+ {
+ var running = true
+ var count = 10
+ while (running && count > 0) {
+ if (kill(signal)) {
+ Thread.sleep(100)
+ count -= 1
+ }
+ else running = false
+ }
+ running
+ }
+
+ def interrupt() { multi_kill("INT") }
+ def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
+
+
+ // JVM shutdown hook
+
+ private val shutdown_hook = new Thread { override def run = terminate() }
+
+ try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
+ catch { case _: IllegalStateException => }
+
+ private def cleanup() =
+ try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
+ catch { case _: IllegalStateException => }
+
+
+ /* result */
+
+ def join: Int = { val rc = proc.waitFor; cleanup(); rc }
+ }
+
+
+ /* bash */
+
+ def bash(script: String): (String, String, Int) =
{
Standard_System.with_tmp_file("isabelle_script") { script_file =>
- Standard_System.with_tmp_file("isabelle_pid") { pid_file =>
- Standard_System.with_tmp_file("isabelle_output") { output_file =>
-
- Standard_System.write_file(script_file, script)
-
- val proc = execute(true, expand_path("$ISABELLE_HOME/lib/scripts/bash"), "group",
- script_file.getPath, pid_file.getPath, output_file.getPath)
-
- def kill(strict: Boolean) =
- {
- val pid =
- try { Some(Standard_System.read_file(pid_file)) }
- catch { case _: IOException => None }
- if (pid.isDefined) {
- var running = true
- var count = 10 // FIXME property!?
- while (running && count > 0) {
- if (execute(true, "kill", "-INT", "-" + pid.get).waitFor != 0)
- running = false
- else {
- Thread.sleep(100) // FIXME property!?
- if (!strict) count -= 1
- }
- }
- }
- }
+ Standard_System.write_file(script_file, script)
+ val proc = new Managed_Process(false, "bash", posix_path(script_file.getPath))
- val shutdown_hook = new Thread { override def run = kill(true) }
- Runtime.getRuntime.addShutdownHook(shutdown_hook) // FIXME tmp files during shutdown?!?
-
- def cleanup() =
- try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
- catch { case _: IllegalStateException => }
+ proc.stdin.close
+ val stdout = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
+ val stderr = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
- val rc =
- try {
- try { proc.waitFor } // FIXME read stderr (!??)
- catch { case e: InterruptedException => Thread.interrupted; kill(false); throw e }
- }
- finally {
- proc.getOutputStream.close
- proc.getInputStream.close
- proc.getErrorStream.close
- proc.destroy
- cleanup()
- }
-
- val output =
- try { Standard_System.read_file(output_file) }
- catch { case _: IOException => "" }
-
- (output, rc)
- }
- }
+ val rc =
+ try { proc.join }
+ catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 }
+ (stdout.join, stderr.join, rc)
}
}
+
+ /* system tools */
+
def isabelle_tool(name: String, args: String*): (String, Int) =
{
getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>
@@ -287,15 +317,12 @@
"FIFO=\"/tmp/isabelle-fifo-${PPID}-$$-" + i + "\"\n" +
"mkfifo -m 600 \"$FIFO\" || { echo \"Failed to create fifo: $FIFO\" >&2; exit 2; }\n" +
"echo -n \"$FIFO\"\n"
- val (result, rc) = bash_output(script)
- if (rc == 0) result
- else error(result)
+ val (out, err, rc) = bash(script)
+ if (rc == 0) out else error(err)
}
- def rm_fifo(fifo: String)
- {
- bash_output("rm -f '" + fifo + "'")
- }
+ def rm_fifo(fifo: String): Boolean =
+ (new File(jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete
def fifo_input_stream(fifo: String): InputStream =
{
--- a/src/Pure/System/session.scala Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Pure/System/session.scala Wed Sep 22 16:24:41 2010 +0200
@@ -41,8 +41,7 @@
/* pervasive event buses */
val global_settings = new Event_Bus[Session.Global_Settings.type]
- val raw_protocol = new Event_Bus[Isabelle_Process.Result]
- val raw_output = new Event_Bus[Isabelle_Process.Result]
+ val raw_messages = new Event_Bus[Isabelle_Process.Result]
val commands_changed = new Event_Bus[Session.Commands_Changed]
val perspective = new Event_Bus[Session.Perspective.type]
val assignments = new Event_Bus[Session.Assignment.type]
@@ -63,7 +62,8 @@
private case object Stop
- private val command_change_buffer = Simple_Thread.actor("command_change_buffer", daemon = true)
+ private val (_, command_change_buffer) =
+ Simple_Thread.actor("command_change_buffer", daemon = true)
//{{{
{
import scala.compat.Platform.currentTime
@@ -115,10 +115,11 @@
private val global_state = new Volatile(Document.State.init)
def current_state(): Document.State = global_state.peek()
+ private case object Interrupt_Prover
private case class Edit_Version(edits: List[Document.Node_Text_Edit])
private case class Started(timeout: Int, args: List[String])
- private val session_actor = Simple_Thread.actor("session_actor", daemon = true)
+ private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
{
var prover: Isabelle_Process with Isar_Document = null
@@ -176,7 +177,7 @@
def handle_result(result: Isabelle_Process.Result)
//{{{
{
- raw_protocol.event(result)
+ raw_messages.event(result)
result.properties match {
case Position.Id(state_id) =>
@@ -201,8 +202,8 @@
}
}
else if (result.is_exit) prover = null // FIXME ??
- else if (result.is_stdout) raw_output.event(result)
- else if (!result.is_system) bad_result(result) // FIXME syslog for system messages (!?)
+ else if (!(result.is_init || result.is_exit || result.is_system || result.is_stdout))
+ bad_result(result)
}
}
//}}}
@@ -216,7 +217,7 @@
while (
receiveWithin(0) {
case result: Isabelle_Process.Result =>
- if (result.is_stdout) {
+ if (result.is_system) {
for (text <- XML.content(result.message))
buf.append(text)
}
@@ -230,6 +231,7 @@
{
receiveWithin(timeout) {
case result: Isabelle_Process.Result if result.is_init =>
+ handle_result(result)
while (receive {
case result: Isabelle_Process.Result =>
handle_result(result); !result.is_ready
@@ -237,10 +239,11 @@
None
case result: Isabelle_Process.Result if result.is_exit =>
+ handle_result(result)
Some(startup_error())
case TIMEOUT => // FIXME clarify
- prover.kill; Some(startup_error())
+ prover.terminate; Some(startup_error())
}
}
@@ -250,6 +253,9 @@
var finished = false
while (!finished) {
receive {
+ case Interrupt_Prover =>
+ if (prover != null) prover.interrupt
+
case Edit_Version(edits) =>
val previous = global_state.peek().history.tip.current
val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
@@ -272,7 +278,7 @@
if (prover == null) {
prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
val origin = sender
- val opt_err = prover_startup(timeout)
+ val opt_err = prover_startup(timeout + 500)
if (opt_err.isDefined) prover = null
origin ! opt_err
}
@@ -281,7 +287,7 @@
case Stop => // FIXME synchronous!?
if (prover != null) {
global_state.change(_ => Document.State.init)
- prover.kill
+ prover.terminate
prover = null
}
@@ -302,6 +308,8 @@
def stop() { command_change_buffer ! Stop; session_actor ! Stop }
+ def interrupt() { session_actor ! Interrupt_Prover }
+
def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
--- a/src/Pure/System/standard_system.scala Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Pure/System/standard_system.scala Wed Sep 22 16:24:41 2010 +0200
@@ -9,7 +9,7 @@
import java.util.regex.Pattern
import java.util.Locale
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
- BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
+ BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
File, FileFilter, IOException}
import scala.io.{Source, Codec}
@@ -77,24 +77,19 @@
/* basic file operations */
- def with_tmp_file[A](prefix: String)(body: File => A): A =
+ def slurp(reader: BufferedReader): String =
{
- val file = File.createTempFile(prefix, null)
- try { body(file) } finally { file.delete }
+ val output = new StringBuilder(100)
+ var c = -1
+ while ({ c = reader.read; c != -1 }) output += c.toChar
+ reader.close
+ output.toString
}
- 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 slurp(stream: InputStream): String =
+ slurp(new BufferedReader(new InputStreamReader(stream, charset)))
+
+ def read_file(file: File): String = slurp(new FileInputStream(file))
def write_file(file: File, text: CharSequence)
{
@@ -103,6 +98,13 @@
finally { writer.close }
}
+ def with_tmp_file[A](prefix: String)(body: File => A): A =
+ {
+ val file = File.createTempFile(prefix, null)
+ file.deleteOnExit
+ try { body(file) } finally { file.delete }
+ }
+
// FIXME handle (potentially cyclic) directory graph
def find_files(start: File, ok: File => Boolean): List[File] =
{
@@ -138,7 +140,7 @@
def process_output(proc: Process): (String, Int) =
{
proc.getOutputStream.close
- val output = Source.fromInputStream(proc.getInputStream)(codec()).mkString // FIXME
+ val output = slurp(proc.getInputStream)
val rc =
try { proc.waitFor }
finally {
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/README.html Wed Sep 22 16:24:41 2010 +0200
@@ -0,0 +1,24 @@
+<?xml version="1.0" encoding="ISO-8859-1" ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+<title>Notes on Isabelle/Isar Prover IDE</title>
+</head>
+
+<body>
+
+<h1>Notes on Isabelle/Isar Prover IDE</h1>
+
+<ul>
+
+<li>FIXME</li>
+
+<li>FIXME</li>
+
+</ul>
+
+</body>
+</html>
+
--- a/src/Tools/jEdit/src/jedit/html_panel.scala Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Wed Sep 22 16:24:41 2010 +0200
@@ -116,6 +116,7 @@
/* internal messages */
private case class Resize(font_family: String, font_size: Int)
+ private case class Render_Document(text: String)
private case class Render(body: XML.Body)
private case object Refresh
@@ -152,6 +153,12 @@
def refresh() { render(current_body) }
+ def render_document(text: String)
+ {
+ val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
+ Swing_Thread.later { setDocument(doc, rcontext) }
+ }
+
def render(body: XML.Body)
{
current_body = body
@@ -179,6 +186,7 @@
react {
case Resize(font_family, font_size) => resize(font_family, font_size)
case Refresh => refresh()
+ case Render_Document(text) => render_document(text)
case Render(body) => render(body)
case bad => System.err.println("main_actor: ignoring bad message " + bad)
}
@@ -190,5 +198,6 @@
def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
def refresh() { main_actor ! Refresh }
+ def render_document(text: String) { main_actor ! Render_Document(text) }
def render(body: XML.Body) { main_actor ! Render(body) }
}
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Wed Sep 22 16:24:41 2010 +0200
@@ -24,7 +24,7 @@
{
Swing_Thread.require()
- val html_panel =
+ private val html_panel =
new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
set_content(html_panel)
@@ -137,7 +137,7 @@
}
update.tooltip = "Update display according to the command at cursor position"
- val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
+ private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
add(controls.peer, BorderLayout.NORTH)
handle_update()
--- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Wed Sep 22 16:24:41 2010 +0200
@@ -34,6 +34,6 @@
}
}
- override def init() { Isabelle.session.raw_protocol += main_actor }
- override def exit() { Isabelle.session.raw_protocol -= main_actor }
+ override def init() { Isabelle.session.raw_messages += main_actor }
+ override def exit() { Isabelle.session.raw_messages -= main_actor }
}
--- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Wed Sep 22 16:24:41 2010 +0200
@@ -29,13 +29,14 @@
loop {
react {
case result: Isabelle_Process.Result =>
- Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
+ if (result.is_stdout)
+ Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
}
}
}
- override def init() { Isabelle.session.raw_output += main_actor }
- override def exit() { Isabelle.session.raw_output -= main_actor }
+ override def init() { Isabelle.session.raw_messages += main_actor }
+ override def exit() { Isabelle.session.raw_messages -= main_actor }
}
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala Wed Sep 22 11:46:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala Wed Sep 22 16:24:41 2010 +0200
@@ -10,16 +10,41 @@
import isabelle._
import scala.actors.Actor._
-import scala.swing.{TextArea, ScrollPane}
+import scala.swing.{FlowPanel, Button, TextArea, ScrollPane, TabbedPane, Component}
+import scala.swing.event.ButtonClicked
+
+import java.awt.BorderLayout
import org.gjt.sp.jedit.View
class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
{
- private val text_area = new TextArea("Isabelle session")
- text_area.editable = false
- set_content(new ScrollPane(text_area))
+ /* main tabs */
+
+ private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 12)
+ readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
+
+ private val syslog = new TextArea
+ syslog.editable = false
+
+ private val tabs = new TabbedPane {
+ pages += new TabbedPane.Page("README", Component.wrap(readme))
+ pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
+ }
+
+ set_content(tabs)
+
+
+ /* controls */
+
+ private val interrupt = new Button("Interrupt") {
+ reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
+ }
+ interrupt.tooltip = "Broadcast interrupt to all prover tasks"
+
+ private val controls = new FlowPanel(FlowPanel.Alignment.Right)(interrupt)
+ add(controls.peer, BorderLayout.NORTH)
/* main actor */
@@ -27,11 +52,15 @@
private val main_actor = actor {
loop {
react {
+ case result: Isabelle_Process.Result =>
+ if (result.is_init || result.is_exit || result.is_system || result.is_ready)
+ Swing_Thread.now { syslog.append(XML.content(result.message).mkString + "\n") }
+
case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
}
}
}
- override def init() { }
- override def exit() { }
+ override def init() { Isabelle.session.raw_messages += main_actor }
+ override def exit() { Isabelle.session.raw_messages -= main_actor }
}