obsolete -- superceded by Pure.jar (Scala version);
authorwenzelm
Sat Aug 23 23:20:43 2008 +0200 (2008-08-23)
changeset 2797612d9ec5b08de
parent 27975 fbec8e89f255
child 27977 74d32406010f
obsolete -- superceded by Pure.jar (Scala version);
lib/classes/isabelle/IsabelleDemo.java
lib/classes/isabelle/IsabelleProcess.java
     1.1 --- a/lib/classes/isabelle/IsabelleDemo.java	Sat Aug 23 23:17:11 2008 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,58 +0,0 @@
     1.4 -/*
     1.5 - * $Id$
     1.6 - *
     1.7 - * Simple demo for IsabelleProcess wrapper.
     1.8 - *
     1.9 - * Example session with Beanshell:
    1.10 - *
    1.11 - *    $ cd [ISABELLE_HOME]/lib/classes
    1.12 - *    $ javac isabelle/*.java
    1.13 - *
    1.14 - *    $ bsh
    1.15 - * or
    1.16 - *    $ java -Disabelle.home=[ISABELLE_HOME] -jar bsh.jar
    1.17 - *    % addClassPath(".");
    1.18 - *
    1.19 - *    % import isabelle.*;
    1.20 - *    % isabelle = new IsabelleDemo("HOL");
    1.21 - *    % isabelle.command("theory Test imports Main begin");
    1.22 - *    % isabelle.command("lemma \"A --> A\"");
    1.23 - *    % isabelle.command("..");
    1.24 - *    % isabelle.command("end");
    1.25 - *    % isabelle.close();
    1.26 - *
    1.27 - */
    1.28 -
    1.29 -package isabelle;
    1.30 -
    1.31 -public class IsabelleDemo extends IsabelleProcess {
    1.32 -    public IsabelleDemo(String logic) throws IsabelleProcessException
    1.33 -    {
    1.34 -        super(logic);
    1.35 -        new Thread (new Runnable () {
    1.36 -            public void run()
    1.37 -            {
    1.38 -                IsabelleProcess.Result result = null;
    1.39 -                do {
    1.40 -                  try {
    1.41 -                    result = results.take();
    1.42 -                  } catch (NullPointerException ex) {
    1.43 -                    result = null;
    1.44 -                  } catch (InterruptedException ex) {
    1.45 -                    result = null;
    1.46 -                  }
    1.47 -                  if (result != null)
    1.48 -                    System.err.println(result.toString());
    1.49 -                  if (result.kind == IsabelleProcess.Result.Kind.EXIT) {
    1.50 -                    result = null;
    1.51 -                  }
    1.52 -                } while (result != null);
    1.53 -                System.err.println("Console thread terminated");
    1.54 -            }
    1.55 -        }).start();
    1.56 -    }
    1.57 -    
    1.58 -    public IsabelleDemo() throws IsabelleProcessException {
    1.59 -        this(null);
    1.60 -    }
    1.61 -}
     2.1 --- a/lib/classes/isabelle/IsabelleProcess.java	Sat Aug 23 23:17:11 2008 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,557 +0,0 @@
     2.4 -/*
     2.5 - * $Id$
     2.6 - */
     2.7 -
     2.8 -package isabelle;
     2.9 -
    2.10 -import java.io.*;
    2.11 -import java.util.Locale;
    2.12 -import java.util.ArrayList;
    2.13 -import java.util.Properties;
    2.14 -import java.util.Enumeration;
    2.15 -import java.util.concurrent.LinkedBlockingQueue;
    2.16 -
    2.17 -/**
    2.18 - * Posix process wrapper for Isabelle (see also <code>src/Pure/Tools/isabelle_process.ML</code>).
    2.19 - * <p>
    2.20 - *
    2.21 - * The process model:
    2.22 - * <p>
    2.23 - *
    2.24 - * <ol>
    2.25 - * <li> input
    2.26 - * <ul>
    2.27 - * <li> stdin stream
    2.28 - * <li> signals (interrupt, kill)
    2.29 - * </ul>
    2.30 - *
    2.31 - * <li> output/results
    2.32 - * <ul>
    2.33 - * <li> stdout stream, interspersed with marked Isabelle messages
    2.34 - * <li> stderr stream
    2.35 - * <li> process init (pid and session property)
    2.36 - * <li> process exit (return code)
    2.37 - * </ul>
    2.38 - * </ol>
    2.39 - *
    2.40 - * I/O is fully asynchronous, with unrestricted buffers.  Text is encoded as UTF-8.
    2.41 - * <p>
    2.42 - *
    2.43 - * System properties:
    2.44 - * <p>
    2.45 - *
    2.46 - * <dl>
    2.47 - * <dt> <code>isabelle.home</code>  <di> <code>ISABELLE_HOME</code> of Isabelle installation
    2.48 - *                      (default determined from isabelle-process via <code>PATH</code>)
    2.49 - * <dt> <code>isabelle.shell</code> <di> optional shell command for <code>isabelle-process</code> (also requires isabelle.home)
    2.50 - * <dt> <code>isabelle.kill</code>  <di> optional kill command (default <code>kill</code>)
    2.51 - */
    2.52 -
    2.53 -public class IsabelleProcess {
    2.54 -    private volatile Process proc = null;
    2.55 -    private volatile String pid = null;
    2.56 -    private volatile boolean closing = false;
    2.57 -    private LinkedBlockingQueue<String> output = null;
    2.58 -
    2.59 -    public volatile String session = null;
    2.60 -
    2.61 -    
    2.62 -    /**
    2.63 -     * Models failures in process management.
    2.64 -     */
    2.65 -    public static class IsabelleProcessException extends Exception {
    2.66 -        public IsabelleProcessException() {
    2.67 -            super();
    2.68 -        }
    2.69 -        public IsabelleProcessException(String msg) {
    2.70 -            super(msg);
    2.71 -        }
    2.72 -    };
    2.73 -
    2.74 -
    2.75 -    /**
    2.76 -     * Models cooked results from the process.
    2.77 -     */
    2.78 -    public static class Result {
    2.79 -        public enum Kind {
    2.80 -            // Posix channels/events
    2.81 -            STDIN, STDOUT, STDERR, SIGNAL, EXIT,
    2.82 -            // Isabelle messages
    2.83 -            WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG, PROMPT, INIT, STATUS,
    2.84 -            // internal system notification
    2.85 -            SYSTEM
    2.86 -        };
    2.87 -        public Kind kind;
    2.88 -        public Properties props;
    2.89 -        public String result;
    2.90 -
    2.91 -        public Result(Kind kind, Properties props, String result) {
    2.92 -            this.kind = kind;
    2.93 -            this.props = props;
    2.94 -            this.result = result;
    2.95 -        }
    2.96 -
    2.97 -        public boolean isRaw() {
    2.98 -            return
    2.99 -              this.kind == Kind.STDOUT ||
   2.100 -              this.kind == Kind.STDERR;
   2.101 -        }
   2.102 -
   2.103 -        public boolean isSystem() {
   2.104 -            return
   2.105 -              this.kind == Kind.STDIN ||
   2.106 -              this.kind == Kind.SIGNAL ||
   2.107 -              this.kind == Kind.EXIT ||
   2.108 -              this.kind == Kind.PROMPT ||
   2.109 -              this.kind == Kind.STATUS ||
   2.110 -              this.kind == Kind.SYSTEM;
   2.111 -        }
   2.112 -
   2.113 -        @Override
   2.114 -        public String toString() {
   2.115 -            if (this.props == null) {
   2.116 -                return this.kind.toString() + " [[" + this.result + "]]";
   2.117 -            } else {
   2.118 -                return this.kind.toString() + " " + props.toString() + " [[" + this.result + "]]";
   2.119 -            }
   2.120 -        }
   2.121 -    }
   2.122 -
   2.123 -
   2.124 -    /**
   2.125 -     * Main result queue -- accumulates cooked messages asynchronously.
   2.126 -     */
   2.127 -    public LinkedBlockingQueue<Result> results;
   2.128 -
   2.129 -    private synchronized void putResult(Result.Kind kind, Properties props, String result) {
   2.130 -        try {
   2.131 -            results.put(new Result(kind, props, result));
   2.132 -        } catch (InterruptedException exn) {  }
   2.133 -    }
   2.134 -    private synchronized void putResult(Result.Kind kind, String result) {
   2.135 -        putResult(kind, null, result);
   2.136 -    }
   2.137 -
   2.138 -
   2.139 -    /**
   2.140 -     * Interrupts Isabelle process via Posix signal.
   2.141 -     * @throws isabelle.IsabelleProcess.IsabelleProcessException
   2.142 -     */
   2.143 -    public synchronized void interrupt() throws IsabelleProcessException
   2.144 -    {
   2.145 -        if (proc != null && pid != null) {
   2.146 -            String kill = System.getProperty("isabelle.kill", "kill");
   2.147 -            String [] cmdline = {kill, "-INT", pid};
   2.148 -            try {
   2.149 -                putResult(Result.Kind.SIGNAL, "INT");
   2.150 -                int rc = Runtime.getRuntime().exec(cmdline).waitFor();
   2.151 -                if (rc != 0) {
   2.152 -                    throw new IsabelleProcessException("Cannot interrupt: kill command failed");
   2.153 -                }
   2.154 -            } catch (IOException exn) {
   2.155 -                throw new IsabelleProcessException(exn.getMessage());
   2.156 -            } catch (InterruptedException exn) {
   2.157 -                throw new IsabelleProcessException("Cannot interrupt: aborted");
   2.158 -            }
   2.159 -        } else {
   2.160 -            throw new IsabelleProcessException("Cannot interrupt: no process");
   2.161 -        }
   2.162 -    }
   2.163 -
   2.164 -
   2.165 -    /**
   2.166 -     * Kills Isabelle process: try close -- sleep -- destroy.
   2.167 -     */
   2.168 -    public synchronized void kill() throws IsabelleProcessException
   2.169 -    {
   2.170 -        if (proc != null) {
   2.171 -            tryClose();
   2.172 -            try {
   2.173 -                Thread.sleep(300);
   2.174 -            } catch (InterruptedException exn) { }
   2.175 -            putResult(Result.Kind.SIGNAL, "KILL");
   2.176 -            proc.destroy();
   2.177 -            proc = null;
   2.178 -        } else {
   2.179 -            throw new IsabelleProcessException("Cannot kill: no process");
   2.180 -        }
   2.181 -    }
   2.182 -
   2.183 -    
   2.184 -    /**
   2.185 -     * Models basic Isabelle properties
   2.186 -     */
   2.187 -    public static class Property {
   2.188 -        public static String ID = "id";
   2.189 -        public static String LINE = "line";
   2.190 -        public static String FILE = "file";
   2.191 -    }
   2.192 -
   2.193 -    /**
   2.194 -     * Auxiliary operation to encode text as Isabelle string token.
   2.195 -     */
   2.196 -    public static String encodeString(String str) {
   2.197 -        Locale locale = null;
   2.198 -        StringBuffer buf = new StringBuffer(100);
   2.199 -        int i;
   2.200 -        char c;
   2.201 -
   2.202 -        buf.append("\"");
   2.203 -        for (i = 0; i < str.length(); i++) {
   2.204 -            c = str.charAt(i);
   2.205 -            if (c < 32 || c == '\\' || c == '\"') {
   2.206 -                buf.append(String.format(locale, "\\%03d", (int) c));
   2.207 -            } else {
   2.208 -                buf.append(c);
   2.209 -            }
   2.210 -        }
   2.211 -        buf.append("\"");
   2.212 -        return buf.toString();
   2.213 -    }
   2.214 -
   2.215 -    /**
   2.216 -     * Auxiliary operation to encode properties as Isabelle outer syntax.
   2.217 -     */
   2.218 -    public static String encodeProperties(Properties props) {
   2.219 -        StringBuffer buf = new StringBuffer(100);
   2.220 -        buf.append("(");
   2.221 -        for (Enumeration<String> e = (Enumeration<String>) props.propertyNames(); e.hasMoreElements(); ) {
   2.222 -          String x = e.nextElement();
   2.223 -          buf.append(encodeString(x));
   2.224 -          buf.append(" = ");
   2.225 -          buf.append(encodeString(props.getProperty(x)));
   2.226 -          if (e.hasMoreElements()) {
   2.227 -              buf.append(", ");
   2.228 -          }
   2.229 -        }
   2.230 -        buf.append(")");
   2.231 -        return buf.toString();
   2.232 -    }
   2.233 -
   2.234 -
   2.235 -    /* output being piped into the process (stdin) */
   2.236 -
   2.237 -    private volatile BufferedWriter outputWriter;
   2.238 -    private class OutputThread extends Thread
   2.239 -    {
   2.240 -        public void run()
   2.241 -        {
   2.242 -            while (outputWriter != null) {
   2.243 -                try {
   2.244 -                    String s = output.take();
   2.245 -                    if (s.equals("\u0000")) {
   2.246 -                        outputWriter.close();
   2.247 -                        outputWriter = null;
   2.248 -                    } else {
   2.249 -                        putResult(Result.Kind.STDIN, s);
   2.250 -                        outputWriter.write(s);
   2.251 -                        outputWriter.flush();
   2.252 -                    }
   2.253 -                } catch (InterruptedException exn) {
   2.254 -                    putResult(Result.Kind.SYSTEM, "Output thread interrupted");
   2.255 -                } catch (IOException exn) {
   2.256 -                    putResult(Result.Kind.SYSTEM, exn.getMessage() + " (output thread)");
   2.257 -                }
   2.258 -            }
   2.259 -            putResult(Result.Kind.SYSTEM, "Output thread terminated");
   2.260 -        }
   2.261 -    }
   2.262 -    private OutputThread outputThread;
   2.263 -
   2.264 -
   2.265 -    // public operations
   2.266 -
   2.267 -    /**
   2.268 -     * Feeds arbitrary text into the process.
   2.269 -     */
   2.270 -    public synchronized void output(String text) throws IsabelleProcessException
   2.271 -    {
   2.272 -        if (proc != null && !closing) {
   2.273 -            try {
   2.274 -                output.put(text);
   2.275 -            } catch (InterruptedException ex) {
   2.276 -               throw new IsabelleProcessException("Cannot output: aborted");
   2.277 -            }
   2.278 -        } else if (proc == null) {
   2.279 -            throw new IsabelleProcessException("Cannot output: no process");
   2.280 -        } else {
   2.281 -            throw new IsabelleProcessException("Cannot output: already closing");
   2.282 -        }
   2.283 -    }
   2.284 -
   2.285 -    /**
   2.286 -     * Closes Isabelle process input, causing termination eventually.
   2.287 -     */
   2.288 -    public synchronized void close() throws IsabelleProcessException
   2.289 -    {
   2.290 -        output("\u0000");
   2.291 -        closing = true;
   2.292 -        // FIXME watchdog/timeout
   2.293 -    }
   2.294 -
   2.295 -    /**
   2.296 -     * Closes Isabelle process input, causing termination eventually -- unless process already terminated.
   2.297 -     */
   2.298 -    public synchronized void tryClose()
   2.299 -    {
   2.300 -        if (proc != null && !closing) {
   2.301 -            try {
   2.302 -                close();
   2.303 -            } catch (IsabelleProcessException ex) {  }
   2.304 -        }
   2.305 -    }
   2.306 -
   2.307 -    private synchronized void outputSync(String text) throws IsabelleProcessException
   2.308 -    {
   2.309 -        output(" \\<^sync>\n; " + text + " \\<^sync>;\n");
   2.310 -    }
   2.311 -
   2.312 -    /**
   2.313 -     * Feeds exactly one Isabelle command into the process.
   2.314 -     */
   2.315 -    public synchronized void command(String text) throws IsabelleProcessException
   2.316 -    {
   2.317 -        outputSync("Isabelle.command " + encodeString(text));
   2.318 -    }
   2.319 -
   2.320 -    /**
   2.321 -     * Isabelle command with properties.
   2.322 -     */
   2.323 -    public synchronized void command(Properties props, String text) throws IsabelleProcessException
   2.324 -    {
   2.325 -        outputSync("Isabelle.command " + encodeProperties(props) + " " + encodeString(text));
   2.326 -    }
   2.327 -
   2.328 -    /**
   2.329 -     * Feeds ML toplevel declarations into the process.
   2.330 -     */
   2.331 -    public synchronized void ML(String text) throws IsabelleProcessException
   2.332 -    {
   2.333 -        outputSync("ML_val " + encodeString(text));
   2.334 -    }
   2.335 -
   2.336 -    /**
   2.337 -     * ML command with properties.
   2.338 -     */
   2.339 -    public synchronized void ML(Properties props, String text) throws IsabelleProcessException
   2.340 -    {
   2.341 -        command(props, "ML_val " + encodeString(text));
   2.342 -    }
   2.343 -
   2.344 -
   2.345 -    /* input from the process (stdout/stderr) */
   2.346 -
   2.347 -    private volatile BufferedReader inputReader;
   2.348 -    private class InputThread extends Thread
   2.349 -    {
   2.350 -        public void run()
   2.351 -        {
   2.352 -            Result.Kind kind = Result.Kind.STDOUT;
   2.353 -            Properties props = null;
   2.354 -            StringBuffer buf = new StringBuffer(100);
   2.355 -
   2.356 -            try {
   2.357 -                while (inputReader != null) {
   2.358 -                    if (kind == Result.Kind.STDOUT) {
   2.359 -                        // char mode
   2.360 -                        int c = -1;
   2.361 -                        while ((buf.length() == 0 || inputReader.ready()) &&
   2.362 -                                  (c = inputReader.read()) > 0 && c != 2) {
   2.363 -                            buf.append((char) c);
   2.364 -                        }
   2.365 -                        if (buf.length() > 0) {
   2.366 -                            putResult(kind, buf.toString());
   2.367 -                            buf = new StringBuffer(100);
   2.368 -                        }
   2.369 -                        if (c == -1) {
   2.370 -                            inputReader.close();
   2.371 -                            inputReader = null;
   2.372 -                            tryClose();
   2.373 -                        }
   2.374 -                        else if (c == 2) {
   2.375 -                            c = inputReader.read();
   2.376 -                            switch (c) {
   2.377 -                                case 'A': kind = Result.Kind.WRITELN; break;
   2.378 -                                case 'B': kind = Result.Kind.PRIORITY; break;
   2.379 -                                case 'C': kind = Result.Kind.TRACING; break;
   2.380 -                                case 'D': kind = Result.Kind.WARNING; break;
   2.381 -                                case 'E': kind = Result.Kind.ERROR; break;
   2.382 -                                case 'F': kind = Result.Kind.DEBUG; break;
   2.383 -                                case 'G': kind = Result.Kind.PROMPT; break;
   2.384 -                                case 'H': kind = Result.Kind.INIT; break;
   2.385 -                                case 'I': kind = Result.Kind.STATUS; break;
   2.386 -                                default: kind = Result.Kind.STDOUT; break;
   2.387 -                            }
   2.388 -                            props = null;
   2.389 -                        }
   2.390 -                    } else {
   2.391 -                        // line mode
   2.392 -                        String line = null;
   2.393 -                        if ((line = inputReader.readLine()) != null) {
   2.394 -                            int len = line.length();
   2.395 -                            // property
   2.396 -                            if (line.endsWith("\u0002,")) {
   2.397 -                                int i = line.indexOf("=");
   2.398 -                                if (i > 0) {
   2.399 -                                    String name = line.substring(0, i);
   2.400 -                                    String value = line.substring(i + 1, len - 2);
   2.401 -                                    if (props == null)
   2.402 -                                        props = new Properties();
   2.403 -                                    if (!props.containsKey(name)) {
   2.404 -                                        props.setProperty(name, value);
   2.405 -                                    }
   2.406 -                                }
   2.407 -                            }
   2.408 -                            // last text line
   2.409 -                            else if (line.endsWith("\u0002.")) {
   2.410 -                                if (kind == Result.Kind.INIT && props != null) {
   2.411 -                                    pid = props.getProperty("pid");
   2.412 -                                    session = props.getProperty("session");
   2.413 -                                }
   2.414 -                                buf.append(line.substring(0, len - 2));
   2.415 -                                putResult(kind, props, buf.toString());
   2.416 -                                buf = new StringBuffer(100);
   2.417 -                                kind = Result.Kind.STDOUT;
   2.418 -                            }
   2.419 -                            // text line
   2.420 -                            else {
   2.421 -                                buf.append(line);
   2.422 -                                buf.append("\n");
   2.423 -                            }
   2.424 -                        } else {
   2.425 -                            inputReader.close();
   2.426 -                            inputReader = null;
   2.427 -                            tryClose();
   2.428 -                        }
   2.429 -                    }
   2.430 -                }
   2.431 -            } catch (IOException exn) {
   2.432 -                putResult(Result.Kind.SYSTEM, exn.getMessage() + " (input thread)");
   2.433 -            }
   2.434 -            putResult(Result.Kind.SYSTEM, "Input thread terminated");
   2.435 -        }
   2.436 -    }
   2.437 -    private InputThread inputThread;
   2.438 -
   2.439 -    private volatile BufferedReader errorReader;
   2.440 -    private class ErrorThread extends Thread
   2.441 -    {
   2.442 -        public void run()
   2.443 -        {
   2.444 -            try {
   2.445 -                while (errorReader != null) {
   2.446 -                    StringBuffer buf = new StringBuffer(100);
   2.447 -                    int c;
   2.448 -                    while ((buf.length() == 0 || errorReader.ready()) && (c = errorReader.read()) > 0) {
   2.449 -                        buf.append((char) c);
   2.450 -                    }
   2.451 -                    if (buf.length() > 0) {
   2.452 -                        putResult(Result.Kind.STDERR, buf.toString());
   2.453 -                    } else {
   2.454 -                        errorReader.close();
   2.455 -                        errorReader = null;
   2.456 -                        tryClose();
   2.457 -                    }
   2.458 -                }
   2.459 -            } catch (IOException exn) {
   2.460 -                putResult(Result.Kind.SYSTEM, exn.getMessage() + " (error thread)");
   2.461 -            }
   2.462 -            putResult(Result.Kind.SYSTEM, "Error thread terminated");
   2.463 -        }
   2.464 -    }
   2.465 -    private ErrorThread errorThread;
   2.466 -
   2.467 -
   2.468 -    /* exit thread */
   2.469 -
   2.470 -    private class ExitThread extends Thread
   2.471 -    {
   2.472 -        public void run()
   2.473 -        {
   2.474 -            try {
   2.475 -                int rc = proc.waitFor();
   2.476 -                Thread.sleep(300);
   2.477 -                putResult(Result.Kind.SYSTEM, "Exit thread terminated");
   2.478 -                putResult(Result.Kind.EXIT, Integer.toString(rc));
   2.479 -                proc = null;
   2.480 -            } catch (InterruptedException exn) {
   2.481 -                putResult(Result.Kind.SYSTEM, "Exit thread interrupted");
   2.482 -            }
   2.483 -        }
   2.484 -    }
   2.485 -    private ExitThread exitThread;
   2.486 -
   2.487 -
   2.488 -    /**
   2.489 -     * Creates Isabelle process with specified logic image.
   2.490 -     */
   2.491 -    public IsabelleProcess(String [] options, String logic) throws IsabelleProcessException
   2.492 -    {
   2.493 -        ArrayList<String> cmdline = new ArrayList<String> ();
   2.494 -        String shell = null;
   2.495 -        String home = null;
   2.496 -        String charset = "UTF-8";
   2.497 -
   2.498 -        shell = System.getProperty("isabelle.shell");
   2.499 -        home = System.getProperty("isabelle.home");
   2.500 -        if (shell != null && home != null) {
   2.501 -            cmdline.add(shell);
   2.502 -            cmdline.add(home +  "/bin/isabelle-process");
   2.503 -        } else if (home != null) {
   2.504 -            cmdline.add(home +  "/bin/isabelle-process");
   2.505 -        } else if (shell != null) {
   2.506 -            throw new IsabelleProcessException("Cannot start process: isabelle.shell property requires isabelle.home");
   2.507 -        } else {
   2.508 -            cmdline.add("isabelle-process");
   2.509 -        }
   2.510 -        cmdline.add("-W");
   2.511 -        if (options != null) {
   2.512 -            for (String opt: options) cmdline.add(opt);
   2.513 -        }
   2.514 -        if (logic != null) cmdline.add(logic);
   2.515 -
   2.516 -        try {
   2.517 -            String [] cmd = new String[cmdline.size()];
   2.518 -            cmdline.toArray(cmd);
   2.519 -            proc = Runtime.getRuntime().exec(cmd);
   2.520 -        } catch (IOException exn) {
   2.521 -            throw new IsabelleProcessException(exn.getMessage());
   2.522 -        }
   2.523 -
   2.524 -        try {
   2.525 -            outputWriter = new BufferedWriter(new OutputStreamWriter(proc.getOutputStream(), charset));
   2.526 -            inputReader = new BufferedReader(new InputStreamReader(proc.getInputStream(), charset));
   2.527 -            errorReader = new BufferedReader(new InputStreamReader(proc.getErrorStream(), charset));
   2.528 -        } catch (UnsupportedEncodingException exn) {
   2.529 -            proc.destroy();
   2.530 -            throw new Error(exn.getMessage());
   2.531 -        }
   2.532 -
   2.533 -        output = new LinkedBlockingQueue<String>();
   2.534 -        outputThread = new OutputThread();
   2.535 -
   2.536 -        results = new LinkedBlockingQueue<Result>();
   2.537 -        inputThread = new InputThread();
   2.538 -        errorThread = new ErrorThread();
   2.539 -        exitThread = new ExitThread();
   2.540 -
   2.541 -        outputThread.start();
   2.542 -        inputThread.start();
   2.543 -        errorThread.start();
   2.544 -        exitThread.start();
   2.545 -    }
   2.546 -
   2.547 -    /**
   2.548 -     * Creates Isabelle process without options.
   2.549 -     */
   2.550 -    public IsabelleProcess(String logic) throws IsabelleProcessException {
   2.551 -        this(null, logic);
   2.552 -    }
   2.553 -
   2.554 -    /**
   2.555 -     * Creates Isabelle process with default logic image.
   2.556 -     */
   2.557 -    public IsabelleProcess() throws IsabelleProcessException {
   2.558 -        this(null);
   2.559 -    }
   2.560 -}