more explicit treatment of return code vs. session phase;

--- a/src/Pure/PIDE/isabelle_markup.scala	Tue May 29 17:54:34 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Tue May 29 18:00:54 2012 +0200
@@ -236,6 +236,8 @@
   val STDERR = "stderr"
   val EXIT = "exit"
 
+  val Return_Code = new Properties.Int("return_code")
+
   val LEGACY = "legacy"
 
   val NO_REPORT = "no_report"

--- a/src/Pure/System/isabelle_process.scala	Tue May 29 17:54:34 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue May 29 18:00:54 2012 +0200
@@ -104,9 +104,10 @@
     }
   }
 
-  private def output_message(kind: String, text: String)
+  private def exit_message(rc: Int)
   {
-    output_message(kind, Nil, List(XML.Text(Symbol.decode(text))))
+    output_message(Isabelle_Markup.EXIT, Isabelle_Markup.Return_Code(rc),
+      List(XML.Text("Return code: " + rc.toString)))
   }
 
 
@@ -172,7 +173,7 @@
     if (startup_errors != "") system_output(startup_errors)
 
     if (startup_failed) {
-      output_message(Isabelle_Markup.EXIT, "Return code: 127")
+      exit_message(127)
       process.stdin.close
       Thread.sleep(300)
       terminate_process()
@@ -192,7 +193,7 @@
       for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
         thread.join
       system_output("process_manager terminated")
-      output_message(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
+      exit_message(rc)
     }
     system_channel.accepted()
   }
@@ -263,7 +264,7 @@
             else done = true
           }
           if (result.length > 0) {
-            output_message(markup, result.toString)
+            output_message(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
             result.length = 0
           }
           else {

--- a/src/Pure/System/session.scala	Tue May 29 17:54:34 2012 +0200
+++ b/src/Pure/System/session.scala	Tue May 29 18:00:54 2012 +0200
@@ -369,10 +369,12 @@
         case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
           prover_syntax += name
 
+        case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
+          if (rc == 0) phase = Session.Inactive
+          else phase = Session.Failed
+
         case _ =>
-          if (output.is_exit && phase == Session.Startup) phase = Session.Failed
-          else if (output.is_exit) phase = Session.Inactive
-          else if (output.is_init || output.is_stdout) { }
+          if (output.is_init || output.is_stdout) { }
           else bad_output(output)
       }
     }