# HG changeset patch
# User wenzelm
# Date 1219525664 -7200
# Node ID 18d02c0b90b6e9b065a0b681985a551fb9048d0e
# Parent  a87be8fcb25c7eaaf47fdfeba221abecc438b750
moved class Result into static object, removed dynamic tree method;
removed unused Symbol.Interpretation;
class Result: added is_raw, is_system;
disabled console echo;
added interrupt, kill;
IsabelleSystem.exec;

diff -r a87be8fcb25c -r 18d02c0b90b6 src/Pure/Tools/isabelle_process.scala
--- a/src/Pure/Tools/isabelle_process.scala	Sat Aug 23 23:07:43 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.scala	Sat Aug 23 23:07:44 2008 +0200
@@ -16,27 +16,15 @@
 import isabelle.{Symbol, XML}
 
 
-class IsabelleProcess(args: String*) {
+object IsabelleProcess {
+
+  /* exception */
 
   class IsabelleProcessException(msg: String) extends Exception {
     override def toString = "IsabelleProcess: " + msg
   }
 
 
-  /* process information */
-
-  private var proc: Process = null
-  private var closing = false
-  private var pid: String = null
-  private var session: String = null
-
-
-  /* encoding */
-
-  private val charset = "UTF-8"
-  private val symbols = new Symbol.Interpretation
-
-
   /* results */
 
   object Kind extends Enumeration {
@@ -72,36 +60,75 @@
       kind == SYSTEM
   }
 
-  class Result(kind: Kind.Value, props: Properties, result: String) {
-    //{{{
+  class Result(val kind: Kind.Value, val props: Properties, val result: String) {
     override def toString = {
       val res = XML.content(YXML.parse_failsafe(result)).mkString("")
       if (props == null) kind.toString + " [[" + res + "]]"
       else kind.toString + " " + props.toString + " [[" + res + "]]"
     }
+    def is_raw() = Kind.is_raw(kind)
+    def is_system() = Kind.is_system(kind)
+  }
 
-    private var the_tree: XML.Tree = null
-    def tree() = synchronized {
-      if (the_tree == null) {
-        val t = YXML.parse_failsafe(symbols.decode(result))
-        the_tree = if (Kind.is_raw(kind)) XML.Elem(Markup.RAW, Nil, List(t)) else t
-      }
-      the_tree
-    }
-    //}}}
-  }
+}
+
+
+class IsabelleProcess(args: String*) {
+
+  import IsabelleProcess._
+
+
+  /* process information */
+
+  private var proc: Process = null
+  private var closing = false
+  private var pid: String = null
+  private var the_session: String = null
+  def session() = the_session
+
+
+  /* results */
 
   val results = new LinkedBlockingQueue[Result]
 
   private def put_result(kind: Kind.Value, props: Properties, result: String) {
     if (kind == Kind.INIT && props != null) {
-      pid = props.getProperty("pid")
-      session = props.getProperty("session")
+      pid = props.getProperty(Markup.PID)
+      the_session = props.getProperty(Markup.SESSION)
     }
-    Console.println(new Result(kind, props, result))
     results.put(new Result(kind, props, result))
   }
 
+  val symbols = new Symbol.Interpretation
+  def result_tree(result: Result) = YXML.parse_failsafe(symbols.decode(result.result))
+
+
+  /* signals */
+
+  def interrupt() = synchronized {
+    if (proc == null) throw new IsabelleProcessException("Cannot interrupt: no process")
+    if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
+    else {
+      put_result(Kind.SIGNAL, null, "INT")
+      try {
+        if (IsabelleSystem.exec(List("kill", "-INT", pid)).waitFor != 0)
+          put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
+      }
+      catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
+    }
+  }
+
+  def kill() = synchronized {
+    if (proc == 0) throw new IsabelleProcessException("Cannot kill: no process")
+    else {
+      try_close()
+      Thread.sleep(300)
+      put_result(Kind.SIGNAL, null, "KILL")
+      proc.destroy
+      proc = null
+    }
+  }
+
 
   /* output being piped into the process */
 
@@ -313,29 +340,18 @@
   /** main **/
 
   {
-    /* command line */
-
-    val cmdline = {
-      val cmdline = new ArrayBuffer[String]
+    /* exec process */
 
-      IsabelleSystem.shell_prefix match {
-        case None => ()
-        case Some(prefix) => cmdline + prefix
-      }
-      cmdline + (IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process")
-      cmdline + "-W"
-      for (arg <- args) cmdline + arg
-      cmdline.toArray
+    try {
+      proc = IsabelleSystem.exec(List(
+        IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W") ++ args)
     }
-
-    try { proc = Runtime.getRuntime.exec(cmdline) }
-    catch {
-      case e: IOException => throw new IsabelleProcessException(e.getMessage)
-    }
+    catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
 
 
-    /* process control via threads */
+    /* control process via threads */
 
+    val charset = "UTF-8"
     new StdinThread(new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, charset))).start
     new StdoutThread(new BufferedReader(new InputStreamReader(proc.getInputStream, charset))).start
     new StderrThread(new BufferedReader(new InputStreamReader(proc.getErrorStream, charset))).start
@@ -343,4 +359,3 @@
   }
 
 }
-