# HG changeset patch
# User wenzelm
# Date 1197674642 -3600
# Node ID 7ce14ed29c77282380751b130eb85175051f44cf
# Parent  df9485037438fdd3e0b36e705abf91a2d45fb99f
proper termination of stdout thread;
tuned;

diff -r df9485037438 -r 7ce14ed29c77 lib/classes/isabelle/IsabelleProcess.java
--- a/lib/classes/isabelle/IsabelleProcess.java	Fri Dec 14 23:00:52 2007 +0100
+++ b/lib/classes/isabelle/IsabelleProcess.java	Sat Dec 15 00:24:02 2007 +0100
@@ -22,10 +22,10 @@
 import java.util.concurrent.LinkedBlockingQueue;
 
 public class IsabelleProcess {
-    private volatile Process proc;
-    private volatile String pid;
+    private volatile Process proc = null;
+    private volatile String pid = null;
     private volatile boolean closing = false;
-    private LinkedBlockingQueue<String> output;
+    private LinkedBlockingQueue<String> output = null;
 
 
     /* exceptions */
@@ -97,21 +97,14 @@
     {
         if (proc != null) {
             proc.destroy();
+            proc = null;
         } else {
             throw new IsabelleProcessException("Cannot destroy: no process");
         }
     }
-
+    
     
-    /* terminate process */
-
-    public synchronized void terminate()
-    {
-        // FIXME timeout?
-    }
-
-
-    /* encode arbitrary strings */
+    /* encode text as string token */
     
     public static String encodeString(String str) {
         Locale locale = null;
@@ -144,7 +137,7 @@
                 try {
                     String s = output.take();
                     if (s.equals("\u0000")) {
-                        outputWriter.close();    // FIXME timeout
+                        outputWriter.close();
                         outputWriter = null;
                     } else {
                         outputWriter.write(s);
@@ -165,12 +158,14 @@
     
     public synchronized void output(String text) throws IsabelleProcessException
     {
-        if (!closing) {
+        if (proc != null && !closing) {
             try {
                 output.put(text);
             } catch (InterruptedException ex) {
                throw new IsabelleProcessException("Cannot output: aborted"); 
             }
+        } else if (proc == null) {
+            throw new IsabelleProcessException("Cannot output: no process");
         } else {
             throw new IsabelleProcessException("Cannot output: already closing");
         }
@@ -180,36 +175,37 @@
     {
         output("\u0000");
         closing = true;
+        // FIXME start watchdog
     }
     
-    private synchronized void commandWrapping(String cmd, String text) throws IsabelleProcessException
+    public synchronized void tryClose()
+    {
+        if (proc != null && !closing) {
+            try {
+                close();
+            } catch (IsabelleProcessException ex) {  }
+        }
+    }
+
+    private synchronized void outputWrapped(String cmd, String text) throws IsabelleProcessException
     {
         output(" \\<^sync> " + cmd + " " + encodeString(text) + " \\<^sync>;\n");
     }
 
     public synchronized void command(String text) throws IsabelleProcessException
     {
-        commandWrapping("Isabelle.command", text);
+        outputWrapped("Isabelle.command", text);
     }
 
     public synchronized void ML(String text) throws IsabelleProcessException
     {
-        commandWrapping("ML", text);
+        outputWrapped("ML", text);
     }
 
     
     /* input from the process (stdout/stderr) */
 
     private volatile BufferedReader inputReader;
-    private volatile BufferedReader errorReader;
-
-    private synchronized void checkTermination()
-    {
-        if (inputReader == null && errorReader == null) {
-            terminate();
-        }
-    }
-
     private class InputThread extends Thread
     {
         public void run()
@@ -221,7 +217,7 @@
                 while (inputReader != null) {
                     if (kind == Result.Kind.STDOUT && pid != null) {
                         // char mode
-                        int c = 0;
+                        int c = -1;
                         while ((buf.length() == 0 || inputReader.ready()) &&
                                   (c = inputReader.read()) > 0 && c != 2) {
                             buf.append((char) c);
@@ -242,6 +238,11 @@
                                 default: kind = Result.Kind.STDOUT; break;
                             }
                         }
+                        if (c == -1) {
+                            inputReader.close();
+                            inputReader = null;
+                            tryClose();
+                        }
                     } else {
                         // line mode
                         String line = null;
@@ -268,7 +269,7 @@
                         } else {
                             inputReader.close();
                             inputReader = null;
-                            checkTermination();
+                            tryClose();
                         }
                     }
                 }
@@ -280,6 +281,7 @@
     }
     private InputThread inputThread;
 
+    private volatile BufferedReader errorReader;
     private class ErrorThread extends Thread
     {
         public void run()
@@ -296,7 +298,7 @@
                     } else {
                         errorReader.close();
                         errorReader = null;
-                        checkTermination();
+                        tryClose();
                     }
                 }
             } catch (IOException exn) {
@@ -316,7 +318,8 @@
         {
             try {
                 int rc = proc.waitFor();
-                putResult(Result.Kind.EXIT, new Integer(rc).toString());
+                putResult(Result.Kind.EXIT, Integer.toString(rc));
+                proc = null;
             } catch (InterruptedException exn) {
                 putResult(Result.Kind.FAILURE, "Exit thread: interrupted");
             }
@@ -355,30 +358,33 @@
         String charset = "UTF-8";
         try {
             proc = Runtime.getRuntime().exec(cmdline);
-            pid = null;
+        } catch (IOException exn) {
+            throw new IsabelleProcessException(exn.getMessage());
+        }
 
-            output = new LinkedBlockingQueue<String>();
+        try {
             outputWriter = new BufferedWriter(new OutputStreamWriter(proc.getOutputStream(), charset));
-            outputThread = new OutputThread();
-
-            results = new LinkedBlockingQueue<Result>();
             inputReader = new BufferedReader(new InputStreamReader(proc.getInputStream(), charset));
             errorReader = new BufferedReader(new InputStreamReader(proc.getErrorStream(), charset));
-            inputThread = new InputThread();
-            errorThread = new ErrorThread();
-            exitThread = new ExitThread();
+        } catch (UnsupportedEncodingException exn) {
+            proc.destroy();
+            throw new Error(exn.getMessage());
+        }
+
+        output = new LinkedBlockingQueue<String>();
+        outputThread = new OutputThread();
+
+        results = new LinkedBlockingQueue<Result>();
+        inputThread = new InputThread();
+        errorThread = new ErrorThread();
+        exitThread = new ExitThread();
             
-            consoleThread = new ConsoleThread();
-        } catch (IOException exn) {
-            terminate();
-            throw new IsabelleProcessException(exn.getMessage());
-        }
+        consoleThread = new ConsoleThread();
 
         outputThread.start();
         inputThread.start();
         errorThread.start();
         exitThread.start();
-
         consoleThread.start();
     }
 }