1.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 17:46:30 2012 +0200
     1.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 19:16:58 2012 +0200
     1.3 @@ -102,7 +102,6 @@
     1.4    val no_reportN: string val no_report: Markup.T
     1.5    val badN: string val bad: Markup.T
     1.6    val functionN: string
     1.7 -  val ready: Properties.T
     1.8    val assign_execs: Properties.T
     1.9    val removed_versions: Properties.T
    1.10    val invoke_scala: string -> string -> Properties.T
    1.11 @@ -305,8 +304,6 @@
    1.12  
    1.13  val functionN = "function"
    1.14  
    1.15 -val ready = [(functionN, "ready")];
    1.16 -
    1.17  val assign_execs = [(functionN, "assign_execs")];
    1.18  val removed_versions = [(functionN, "removed_versions")];
    1.19  

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

     3.1 --- a/src/Pure/System/isabelle_process.ML	Tue Aug 07 17:46:30 2012 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Aug 07 19:16:58 2012 +0200
     3.3 @@ -2,17 +2,15 @@
     3.4      Author:     Makarius
     3.5  
     3.6  Isabelle process wrapper, based on private fifos for maximum
     3.7 -robustness and performance.
     3.8 +robustness and performance, or local socket for maximum portability.
     3.9  
    3.10  Startup phases:
    3.11 -  . raw Posix process startup with uncontrolled output on stdout/stderr
    3.12 -  . stderr \002: ML running
    3.13 -  .. stdin/stdout/stderr freely available (raw ML loop)
    3.14 -  .. protocol thread initialization
    3.15 -  ... rendezvous on system channel
    3.16 -  ... message INIT(pid): channels ready
    3.17 -  ... message RAW(keywords)
    3.18 -  ... message RAW(ready): main loop ready
    3.19 +  - raw Posix process startup with uncontrolled output on stdout/stderr
    3.20 +  - stderr \002: ML running
    3.21 +  - stdin/stdout/stderr freely available (raw ML loop)
    3.22 +  - protocol thread initialization
    3.23 +  - rendezvous on system channel
    3.24 +  - message INIT: channels ready
    3.25  *)
    3.26  
    3.27  signature ISABELLE_PROCESS =
    3.28 @@ -96,7 +94,7 @@
    3.29  
    3.30  in
    3.31  
    3.32 -fun setup_channels channel =
    3.33 +fun init_channels channel =
    3.34    let
    3.35      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
    3.36      val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
    3.37 @@ -181,9 +179,7 @@
    3.38            |> fold (update op =) [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]);
    3.39  
    3.40      val channel = rendezvous ();
    3.41 -    val _ = setup_channels channel;
    3.42 -
    3.43 -    val _ = Output.protocol_message Isabelle_Markup.ready "";
    3.44 +    val _ = init_channels channel;
    3.45    in loop channel end));
    3.46  
    3.47  fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);

     4.1 --- a/src/Pure/System/session.scala	Tue Aug 07 17:46:30 2012 +0200
     4.2 +++ b/src/Pure/System/session.scala	Tue Aug 07 19:16:58 2012 +0200
     4.3 @@ -351,16 +351,16 @@
     4.4          case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
     4.5            System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
     4.6  
     4.7 -        case Isabelle_Markup.Ready if output.is_protocol =>
     4.8 +        case _ if output.is_init =>
     4.9              phase = Session.Ready
    4.10  
    4.11          case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
    4.12            if (rc == 0) phase = Session.Inactive
    4.13            else phase = Session.Failed
    4.14  
    4.15 -        case _ =>
    4.16 -          if (output.is_init || output.is_stdout) { }
    4.17 -          else bad_output(output)
    4.18 +        case _ if output.is_stdout =>
    4.19 +
    4.20 +        case _ => bad_output(output)
    4.21        }
    4.22      }
    4.23      //}}}