# HG changeset patch
# User wenzelm
# Date 1285156068 -7200
# Node ID 00be8711082f4826981b50070cb4fb93308e7e4c
# Parent  f2a10986e85afca6926f7fefd2c3316028bcfc57
main Isabelle_Process via Isabelle_System.Managed_Process;
simplified init message: no pid;
misc tuning and simplification;

diff -r f2a10986e85a -r 00be8711082f src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Wed Sep 22 12:52:35 2010 +0200
+++ b/src/Pure/General/markup.ML	Wed Sep 22 13:47:48 2010 +0200
@@ -114,7 +114,6 @@
   val execN: string
   val assignN: string val assign: int -> T
   val editN: string val edit: int -> int -> T
-  val pidN: string
   val serialN: string
   val promptN: string val prompt: T
   val readyN: string val ready: T
@@ -340,7 +339,6 @@
 
 (* messages *)
 
-val pidN = "pid";
 val serialN = "serial";
 
 val (promptN, prompt) = markup_elem "prompt";
diff -r f2a10986e85a -r 00be8711082f src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Wed Sep 22 12:52:35 2010 +0200
+++ b/src/Pure/General/markup.scala	Wed Sep 22 13:47:48 2010 +0200
@@ -227,7 +227,6 @@
 
   /* messages */
 
-  val PID = "pid"
   val Serial = new Long_Property("serial")
 
   val MESSAGE = "message"
diff -r f2a10986e85a -r 00be8711082f src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Wed Sep 22 12:52:35 2010 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Wed Sep 22 13:47:48 2010 +0200
@@ -111,9 +111,6 @@
 val cd = OS.FileSys.chDir;
 val pwd = OS.FileSys.getDir;
 
-fun process_id () =
-  Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));
-
 
 (* getenv *)
 
diff -r f2a10986e85a -r 00be8711082f src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Wed Sep 22 12:52:35 2010 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Sep 22 13:47:48 2010 +0200
@@ -172,9 +172,6 @@
 
 val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
 
-fun process_id pid =
-  Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));
-
 
 (* getenv *)
 
diff -r f2a10986e85a -r 00be8711082f src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Sep 22 12:52:35 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Sep 22 13:47:48 2010 +0200
@@ -78,7 +78,7 @@
       (Position.properties_of (Position.thread_data ()))) body;
 
 fun init_message out_stream =
-  message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
+  message out_stream "A" [] (Session.welcome ());
 
 end;
 
diff -r f2a10986e85a -r 00be8711082f src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Wed Sep 22 12:52:35 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Wed Sep 22 13:47:48 2010 +0200
@@ -92,14 +92,7 @@
 
   private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
   {
-    if (pid.isEmpty && kind == Markup.INIT) {
-      rm_fifos()
-      props.find(_._1 == Markup.PID).map(_._1) match {
-        case None => system_result("Bad Isabelle process initialization: missing pid")
-        case p => pid = p
-      }
-    }
-
+    if (kind == Markup.INIT) rm_fifos()
     val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
     xml_cache.cache_tree(msg)((message: XML.Tree) =>
       receiver ! new Result(message.asInstanceOf[XML.Elem]))
@@ -117,33 +110,39 @@
   private case class Input_Chunks(chunks: List[Array[Byte]])
 
   private case object Close
-  private def close(a: Actor) { if (a != null) a ! Close }
+  private def close(p: (Thread, Actor))
+  {
+    if (p != null && p._1.isAlive) {
+      p._2 ! Close
+      p._1.join
+    }
+  }
 
-  @volatile private var standard_input: Actor = null
-  @volatile private var command_input: Actor = null
+  @volatile private var standard_input: (Thread, Actor) = null
+  @volatile private var command_input: (Thread, Actor) = null
 
 
-  /* process manager */
+  /** process manager **/
 
   private val in_fifo = system.mk_fifo()
   private val out_fifo = system.mk_fifo()
   private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
 
-  private val proc =
+  private val process =
     try {
       val cmdline =
         List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
-      system.execute(true, cmdline: _*)
+      new system.Managed_Process(true, cmdline: _*)
     }
     catch { case e: IOException => rm_fifos(); throw(e) }
 
-  private val stdout_reader =
-    new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
+  private def terminate_process()
+  {
+    try { process.terminate }
+    catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) }
+  }
 
-  private val stdin_writer =
-    new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
-
-  private val (process_manager, _) = Simple_Thread.actor("process_manager")
+  private val process_manager = Simple_Thread.fork("process_manager")
   {
     val (startup_failed, startup_output) =
     {
@@ -152,8 +151,8 @@
 
       var finished = false
       while (!finished && System.currentTimeMillis() <= expired) {
-        while (!finished && stdout_reader.ready) {
-          val c = stdout_reader.read
+        while (!finished && process.stdout.ready) {
+          val c = process.stdout.read
           if (c == 2) finished = true
           else result += c.toChar
         }
@@ -165,62 +164,45 @@
 
     if (startup_failed) {
       put_result(Markup.EXIT, "127")
-      stdin_writer.close
-      Thread.sleep(300)  // FIXME !?
-      proc.destroy  // FIXME unreliable
+      process.stdin.close
+      Thread.sleep(300)
+      terminate_process()
     }
     else {
       // rendezvous
       val command_stream = system.fifo_output_stream(in_fifo)
       val message_stream = system.fifo_input_stream(out_fifo)
 
-      val stdin = stdin_actor(); standard_input = stdin._2
+      standard_input = stdin_actor()
       val stdout = stdout_actor()
-      val input = input_actor(command_stream); command_input = input._2
+      command_input = input_actor(command_stream)
       val message = message_actor(message_stream)
 
-      val rc = proc.waitFor()
+      val rc = process.join
       system_result("Isabelle process terminated")
-      for ((thread, _) <- List(stdin, stdout, input, message)) thread.join
+      for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join
       system_result("process_manager terminated")
       put_result(Markup.EXIT, rc.toString)
     }
     rm_fifos()
   }
 
-  def join() { process_manager.join() }
-
 
-  /* signals */
+  /* management methods */
 
-  @volatile private var pid: Option[String] = None
+  def join() { process_manager.join() }
 
   def interrupt()
   {
-    pid match {
-      case None => system_result("Cannot interrupt Isabelle: unknown pid")
-      case Some(i) =>
-        try {
-          if (system.execute(true, "kill", "-INT", i).waitFor == 0)
-            system_result("Interrupt Isabelle")
-          else
-            system_result("Cannot interrupt Isabelle: kill command failed")
-        }
-        catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
-    }
+    try { process.interrupt }
+    catch { case e: IOException => system_result("Failed to interrupt Isabelle: " + e.getMessage) }
   }
 
-  def kill()
+  def terminate()
   {
-    val running =
-      try { proc.exitValue; false }
-      catch { case e: java.lang.IllegalThreadStateException => true }
-    if (running) {
-      close()
-      Thread.sleep(500)  // FIXME !?
-      system_result("Kill Isabelle")
-      proc.destroy
-    }
+    close()
+    system_result("Terminating Isabelle process")
+    terminate_process()
   }
 
 
@@ -239,10 +221,10 @@
           //{{{
           receive {
             case Input_Text(text) =>
-              stdin_writer.write(text)
-              stdin_writer.flush
+              process.stdin.write(text)
+              process.stdin.flush
             case Close =>
-              stdin_writer.close
+              process.stdin.close
               finished = true
             case bad => System.err.println(name + ": ignoring bad message " + bad)
           }
@@ -269,8 +251,8 @@
           //{{{
           var c = -1
           var done = false
-          while (!done && (result.length == 0 || stdout_reader.ready)) {
-            c = stdout_reader.read
+          while (!done && (result.length == 0 || process.stdout.ready)) {
+            c = process.stdout.read
             if (c >= 0) result.append(c.asInstanceOf[Char])
             else done = true
           }
@@ -279,7 +261,7 @@
             result.length = 0
           }
           else {
-            stdout_reader.close
+            process.stdout.close
             finished = true
           }
           //}}}
@@ -391,10 +373,10 @@
 
   /** main methods **/
 
-  def input_raw(text: String): Unit = standard_input ! Input_Text(text)
+  def input_raw(text: String): Unit = standard_input._2 ! Input_Text(text)
 
   def input_bytes(name: String, args: Array[Byte]*): Unit =
-    command_input ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
+    command_input._2 ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
 
   def input(name: String, args: String*): Unit =
     input_bytes(name, args.map(Standard_System.string_bytes): _*)
diff -r f2a10986e85a -r 00be8711082f src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Sep 22 12:52:35 2010 +0200
+++ b/src/Pure/System/session.scala	Wed Sep 22 13:47:48 2010 +0200
@@ -241,7 +241,7 @@
           Some(startup_error())
 
         case TIMEOUT =>  // FIXME clarify
-          prover.kill; Some(startup_error())
+          prover.terminate; Some(startup_error())
       }
     }
 
@@ -282,7 +282,7 @@
         case Stop => // FIXME synchronous!?
           if (prover != null) {
             global_state.change(_ => Document.State.init)
-            prover.kill
+            prover.terminate
             prover = null
           }