simplified process startup phases: INIT suffices for is_ready;

--- a/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 17:46:30 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 19:16:58 2012 +0200
@@ -102,7 +102,6 @@
   val no_reportN: string val no_report: Markup.T
   val badN: string val bad: Markup.T
   val functionN: string
-  val ready: Properties.T
   val assign_execs: Properties.T
   val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
@@ -305,8 +304,6 @@
 
 val functionN = "function"
 
-val ready = [(functionN, "ready")];
-
 val assign_execs = [(functionN, "assign_execs")];
 val removed_versions = [(functionN, "removed_versions")];
 

--- a/src/Pure/PIDE/isabelle_markup.scala	Tue Aug 07 17:46:30 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Aug 07 19:16:58 2012 +0200
@@ -250,8 +250,6 @@
   val FUNCTION = "function"
   val Function = new Properties.String(FUNCTION)
 
-  val Ready: Properties.T = List((FUNCTION, "ready"))
-
   val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
   val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
 

--- a/src/Pure/System/isabelle_process.ML	Tue Aug 07 17:46:30 2012 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Aug 07 19:16:58 2012 +0200
@@ -2,17 +2,15 @@
     Author:     Makarius
 
 Isabelle process wrapper, based on private fifos for maximum
-robustness and performance.
+robustness and performance, or local socket for maximum portability.
 
 Startup phases:
-  . raw Posix process startup with uncontrolled output on stdout/stderr
-  . stderr \002: ML running
-  .. stdin/stdout/stderr freely available (raw ML loop)
-  .. protocol thread initialization
-  ... rendezvous on system channel
-  ... message INIT(pid): channels ready
-  ... message RAW(keywords)
-  ... message RAW(ready): main loop ready
+  - raw Posix process startup with uncontrolled output on stdout/stderr
+  - stderr \002: ML running
+  - stdin/stdout/stderr freely available (raw ML loop)
+  - protocol thread initialization
+  - rendezvous on system channel
+  - message INIT: channels ready
 *)
 
 signature ISABELLE_PROCESS =
@@ -96,7 +94,7 @@
 
 in
 
-fun setup_channels channel =
+fun init_channels channel =
   let
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
@@ -181,9 +179,7 @@
           |> fold (update op =) [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]);
 
     val channel = rendezvous ();
-    val _ = setup_channels channel;
-
-    val _ = Output.protocol_message Isabelle_Markup.ready "";
+    val _ = init_channels channel;
   in loop channel end));
 
 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);

--- a/src/Pure/System/session.scala	Tue Aug 07 17:46:30 2012 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 07 19:16:58 2012 +0200
@@ -351,16 +351,16 @@
         case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
           System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
 
-        case Isabelle_Markup.Ready if output.is_protocol =>
+        case _ if output.is_init =>
             phase = Session.Ready
 
         case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
           if (rc == 0) phase = Session.Inactive
           else phase = Session.Failed
 
-        case _ =>
-          if (output.is_init || output.is_stdout) { }
-          else bad_output(output)
+        case _ if output.is_stdout =>
+
+        case _ => bad_output(output)
       }
     }
     //}}}