1.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Thu Jan 05 13:27:50 2012 +0100
     1.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Thu Jan 05 14:15:37 2012 +0100
     1.3 @@ -100,11 +100,11 @@
     1.4    val serialN: string
     1.5    val legacyN: string val legacy: Markup.T
     1.6    val promptN: string val prompt: Markup.T
     1.7 -  val readyN: string val ready: Markup.T
     1.8    val reportN: string val report: Markup.T
     1.9    val no_reportN: string val no_report: Markup.T
    1.10    val badN: string val bad: Markup.T
    1.11    val functionN: string
    1.12 +  val ready: Properties.T
    1.13    val assign_execs: Properties.T
    1.14    val removed_versions: Properties.T
    1.15    val invoke_scala: string -> string -> Properties.T
    1.16 @@ -307,7 +307,6 @@
    1.17  
    1.18  val (legacyN, legacy) = markup_elem "legacy";
    1.19  val (promptN, prompt) = markup_elem "prompt";
    1.20 -val (readyN, ready) = markup_elem "ready";
    1.21  
    1.22  val (reportN, report) = markup_elem "report";
    1.23  val (no_reportN, no_report) = markup_elem "no_report";
    1.24 @@ -319,6 +318,8 @@
    1.25  
    1.26  val functionN = "function"
    1.27  
    1.28 +val ready = [(functionN, "ready")];
    1.29 +
    1.30  val assign_execs = [(functionN, "assign_execs")];
    1.31  val removed_versions = [(functionN, "removed_versions")];
    1.32  

     2.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Thu Jan 05 13:27:50 2012 +0100
     2.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Thu Jan 05 14:15:37 2012 +0100
     2.3 @@ -249,14 +249,14 @@
     2.4  
     2.5    val BAD = "bad"
     2.6  
     2.7 -  val READY = "ready"
     2.8 -
     2.9  
    2.10    /* raw message functions */
    2.11  
    2.12    val FUNCTION = "function"
    2.13    val Function = new Properties.String(FUNCTION)
    2.14  
    2.15 +  val Ready: Properties.T = List((FUNCTION, "ready"))
    2.16 +
    2.17    val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
    2.18    val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
    2.19  

     3.1 --- a/src/Pure/PIDE/protocol.scala	Thu Jan 05 13:27:50 2012 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Jan 05 14:15:37 2012 +0100
     3.3 @@ -101,13 +101,6 @@
     3.4  
     3.5    /* specific messages */
     3.6  
     3.7 -  def is_ready(msg: XML.Tree): Boolean =
     3.8 -    msg match {
     3.9 -      case XML.Elem(Markup(Isabelle_Markup.STATUS, _),
    3.10 -        List(XML.Elem(Markup(Isabelle_Markup.READY, _), _))) => true
    3.11 -      case _ => false
    3.12 -    }
    3.13 -
    3.14   def is_tracing(msg: XML.Tree): Boolean =
    3.15      msg match {
    3.16        case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true

     4.1 --- a/src/Pure/System/isabelle_process.ML	Thu Jan 05 13:27:50 2012 +0100
     4.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Jan 05 14:15:37 2012 +0100
     4.3 @@ -185,7 +185,7 @@
     4.4  
     4.5      val _ = Keyword.status ();
     4.6      val _ = Thy_Info.status ();
     4.7 -    val _ = Output.status (Markup.markup Isabelle_Markup.ready "process ready");
     4.8 +    val _ = Output.raw_message Isabelle_Markup.ready "";
     4.9    in loop channel end));
    4.10  
    4.11  fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);

     5.1 --- a/src/Pure/System/isabelle_process.scala	Thu Jan 05 13:27:50 2012 +0100
     5.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Jan 05 14:15:37 2012 +0100
     5.3 @@ -58,8 +58,7 @@
     5.4      def is_status = kind == Isabelle_Markup.STATUS
     5.5      def is_report = kind == Isabelle_Markup.REPORT
     5.6      def is_raw = kind == Isabelle_Markup.RAW
     5.7 -    def is_ready = Protocol.is_ready(message)
     5.8 -    def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr
     5.9 +    def is_syslog = is_init || is_exit || is_system || is_stderr
    5.10  
    5.11      override def toString: String =
    5.12      {

     6.1 --- a/src/Pure/System/session.scala	Thu Jan 05 13:27:50 2012 +0100
     6.2 +++ b/src/Pure/System/session.scala	Thu Jan 05 14:15:37 2012 +0100
     6.3 @@ -389,18 +389,17 @@
     6.4              val (tag, res) = Invoke_Scala.method(name, arg)
     6.5              prover.get.invoke_scala(id, tag, res)
     6.6            }
     6.7 -        case Isabelle_Markup.Cancel_Scala(id) =>
     6.8 -          System.err.println("cancel_scala " + id)  // FIXME cancel JVM task
     6.9 +        case Isabelle_Markup.Cancel_Scala(id) if result.is_raw =>
    6.10 +          System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
    6.11 +        case Isabelle_Markup.Ready if result.is_raw =>
    6.12 +            // FIXME move to ML side (!?)
    6.13 +            syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
    6.14 +            syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
    6.15 +            phase = Session.Ready
    6.16          case _ =>
    6.17            if (result.is_syslog) {
    6.18              reverse_syslog ::= result.message
    6.19 -            if (result.is_ready) {
    6.20 -              // FIXME move to ML side (!?)
    6.21 -              syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
    6.22 -              syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
    6.23 -              phase = Session.Ready
    6.24 -            }
    6.25 -            else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
    6.26 +            if (result.is_exit && phase == Session.Startup) phase = Session.Failed
    6.27              else if (result.is_exit) phase = Session.Inactive
    6.28            }
    6.29            else if (result.is_stdout) { }