# HG changeset patch
# User wenzelm
# Date 1285165481 -7200
# Node ID 106e8952fd2884048a4bf7a326eb1708f6b9d211
# Parent  e5448cf9a04885a3b5ab7f416b70fabf98b7e3b1# Parent  1a34187f0b97955a776865852abbb7dd20db739c
merged

diff -r e5448cf9a048 -r 106e8952fd28 lib/scripts/bash
--- 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'/;
diff -r e5448cf9a048 -r 106e8952fd28 lib/scripts/feeder.pl
--- 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");
diff -r e5448cf9a048 -r 106e8952fd28 lib/scripts/process
--- /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 $!;
+}
+
diff -r e5448cf9a048 -r 106e8952fd28 src/Pure/Concurrent/simple_thread.scala
--- 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)
   }
 }
 
diff -r e5448cf9a048 -r 106e8952fd28 src/Pure/General/markup.ML
--- 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";
diff -r e5448cf9a048 -r 106e8952fd28 src/Pure/General/markup.scala
--- 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 */
diff -r e5448cf9a048 -r 106e8952fd28 src/Pure/ML-Systems/bash.ML
--- 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
diff -r e5448cf9a048 -r 106e8952fd28 src/Pure/ML-Systems/multithreading_polyml.ML
--- 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
diff -r e5448cf9a048 -r 106e8952fd28 src/Pure/ML-Systems/polyml_common.ML
--- 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 *)
 
diff -r e5448cf9a048 -r 106e8952fd28 src/Pure/ML-Systems/smlnj.ML
--- 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 *)
 
diff -r e5448cf9a048 -r 106e8952fd28 src/Pure/System/isabelle_process.ML
--- 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;
diff -r e5448cf9a048 -r 106e8952fd28 src/Pure/System/isabelle_process.scala
--- 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): _*)
diff -r e5448cf9a048 -r 106e8952fd28 src/Pure/System/isabelle_system.scala
--- 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 =
   {
diff -r e5448cf9a048 -r 106e8952fd28 src/Pure/System/session.scala
--- 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 =
diff -r e5448cf9a048 -r 106e8952fd28 src/Pure/System/standard_system.scala
--- 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 {
diff -r e5448cf9a048 -r 106e8952fd28 src/Tools/jEdit/dist-template/README.html
--- /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>
+
diff -r e5448cf9a048 -r 106e8952fd28 src/Tools/jEdit/src/jedit/html_panel.scala
--- 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) }
 }
diff -r e5448cf9a048 -r 106e8952fd28 src/Tools/jEdit/src/jedit/output_dockable.scala
--- 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()
diff -r e5448cf9a048 -r 106e8952fd28 src/Tools/jEdit/src/jedit/protocol_dockable.scala
--- 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 }
 }
diff -r e5448cf9a048 -r 106e8952fd28 src/Tools/jEdit/src/jedit/raw_output_dockable.scala
--- 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 }
 }
diff -r e5448cf9a048 -r 106e8952fd28 src/Tools/jEdit/src/jedit/session_dockable.scala
--- 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 }
 }