# HG changeset patch
# User wenzelm
# Date 1197717328 -3600
# Node ID 8e001cc72ca84316a35396f958d507bb03a89af9
# Parent  e50550be4dfa65025f59e795acb07830d178e7e4
Result: added STDOUT, SIGNAL;
renamed method destroy to kill;
method kill: close--sleep--destroy;
tuned;

diff -r e50550be4dfa -r 8e001cc72ca8 lib/classes/isabelle/IsabelleProcess.java
--- a/lib/classes/isabelle/IsabelleProcess.java	Sat Dec 15 00:52:17 2007 +0100
+++ b/lib/classes/isabelle/IsabelleProcess.java	Sat Dec 15 12:15:28 2007 +0100
@@ -7,7 +7,7 @@
  *
  *  (1) input
  *    - stdin stream
- *    - signals (interrupt, destroy)
+ *    - signals (interrupt, kill)
  *
  *  (2) output/results
  *    - stdout stream, interspersed with marked Isabelle messages
@@ -44,8 +44,8 @@
 
     public static class Result {
         public enum Kind {
-            STDOUT, STDERR, EXIT,                               // Posix results
-            WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG,  // Isabelle results
+            STDIN, STDOUT, STDERR, SIGNAL, EXIT,                // Posix channels/events
+            WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG,  // Isabelle messages
             FAILURE                                             // process wrapper problem
         };
         public Kind kind;
@@ -76,9 +76,10 @@
     {
         if (proc != null && pid != null) {
             try {
+                putResult(Result.Kind.SIGNAL, "INT");
                 int rc = Runtime.getRuntime().exec("kill -INT " + pid).waitFor();
                 if (rc != 0) {
-                    throw new IsabelleProcessException("Cannot interrupt: kill failed");
+                    throw new IsabelleProcessException("Cannot interrupt: kill command failed");
                 }
             } catch (IOException exn) {
                 throw new IsabelleProcessException(exn.getMessage());
@@ -91,15 +92,20 @@
     }
 
 
-    /* destroy process */
+    /* kill process */
 
-    public synchronized void destroy() throws IsabelleProcessException
+    public synchronized void kill() throws IsabelleProcessException
     {
         if (proc != null) {
+            tryClose();
+            try {
+                Thread.sleep(300);
+            } catch (InterruptedException exn) { }
+            putResult(Result.Kind.SIGNAL, "KILL");
             proc.destroy();
             proc = null;
         } else {
-            throw new IsabelleProcessException("Cannot destroy: no process");
+            throw new IsabelleProcessException("Cannot kill: no process");
         }
     }
 
@@ -140,6 +146,7 @@
                         outputWriter.close();
                         outputWriter = null;
                     } else {
+                        putResult(Result.Kind.STDIN, s);
                         outputWriter.write(s);
                         outputWriter.flush();
                     }
@@ -149,6 +156,7 @@
                     putResult(Result.Kind.FAILURE, exn.getMessage());
                 }
             }
+            System.err.println("Output thread terminated");
         }
     }
     private OutputThread outputThread;
@@ -175,7 +183,7 @@
     {
         output("\u0000");
         closing = true;
-        // FIXME start watchdog
+        // FIXME watchdog/timeout
     }
 
     public synchronized void tryClose()