refined execute, which replaces exec/exec2;
authorwenzelm
Sat, 27 Dec 2008 16:33:50 +0100
changeset 29178 d41ccf3efbfc
parent 29177 0e88d33e8d19
child 29179 f27d63717075
refined execute, which replaces exec/exec2;
src/Pure/Tools/isabelle_process.scala
--- a/src/Pure/Tools/isabelle_process.scala	Sat Dec 27 16:33:19 2008 +0100
+++ b/src/Pure/Tools/isabelle_process.scala	Sat Dec 27 16:33:50 2008 +0100
@@ -125,7 +125,7 @@
     if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
     else {
       try {
-        if (isabelle_system.exec("kill", "-INT", pid).waitFor == 0)
+        if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
           put_result(Kind.SIGNAL, null, "INT")
         else
           put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
@@ -360,7 +360,7 @@
     try {
       val cmdline =
         List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
-      proc = isabelle_system.exec2(cmdline: _*)
+      proc = isabelle_system.execute(true, cmdline: _*)
     }
     catch {
       case e: IOException =>