# HG changeset patch
# User wenzelm
# Date 1284838436 -7200
# Node ID 59ebce09ce6eb2f018efeef15bf88e333afe115d
# Parent  d8971680b0fc656e06bd70dae3b512c100101c50
recovered basic session stop/restart;

diff -r d8971680b0fc -r 59ebce09ce6e src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sat Sep 18 21:10:07 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sat Sep 18 21:33:56 2010 +0200
@@ -163,7 +163,6 @@
           //{{{
           receive {
             case Input_Text(text) =>
-              // FIXME echo input?!
               writer.write(text)
               writer.flush
             case Close =>
@@ -365,5 +364,5 @@
   def input(name: String, args: String*): Unit =
     input_bytes(name, args.map(Standard_System.string_bytes): _*)
 
-  def close(): Unit = command_input ! Close
+  def close(): Unit = { standard_input ! Close; command_input ! Close }
 }
diff -r d8971680b0fc -r 59ebce09ce6e src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Sep 18 21:10:07 2010 +0200
+++ b/src/Pure/System/session.scala	Sat Sep 18 21:33:56 2010 +0200
@@ -247,7 +247,7 @@
     }
 
 
-    /* main loop */
+    /* main loop */  // FIXME proper shutdown
 
     var finished = false
     while (!finished) {
@@ -282,9 +282,9 @@
 
         case Stop => // FIXME synchronous!?
           if (prover != null) {
+            global_state.change(_ => Document.State.init)
             prover.kill
             prover = null
-            finished = true
           }
 
         case TIMEOUT =>  // FIXME clarify