# HG changeset patch
# User wenzelm
# Date 1325769337 -3600
# Node ID 30a69cd8a9a0c9d539fceba286bb93bc0c3154ca
# Parent  f7ee2e5a83dd27c61ba0572c524542a0a49bce34
prefer raw_message for protocol implementation;

diff -r f7ee2e5a83dd -r 30a69cd8a9a0 src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Thu Jan 05 13:27:50 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML	Thu Jan 05 14:15:37 2012 +0100
@@ -100,11 +100,11 @@
   val serialN: string
   val legacyN: string val legacy: Markup.T
   val promptN: string val prompt: Markup.T
-  val readyN: string val ready: Markup.T
   val reportN: string val report: Markup.T
   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
@@ -307,7 +307,6 @@
 
 val (legacyN, legacy) = markup_elem "legacy";
 val (promptN, prompt) = markup_elem "prompt";
-val (readyN, ready) = markup_elem "ready";
 
 val (reportN, report) = markup_elem "report";
 val (no_reportN, no_report) = markup_elem "no_report";
@@ -319,6 +318,8 @@
 
 val functionN = "function"
 
+val ready = [(functionN, "ready")];
+
 val assign_execs = [(functionN, "assign_execs")];
 val removed_versions = [(functionN, "removed_versions")];
 
diff -r f7ee2e5a83dd -r 30a69cd8a9a0 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Thu Jan 05 13:27:50 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala	Thu Jan 05 14:15:37 2012 +0100
@@ -249,14 +249,14 @@
 
   val BAD = "bad"
 
-  val READY = "ready"
-
 
   /* raw message functions */
 
   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"))
 
diff -r f7ee2e5a83dd -r 30a69cd8a9a0 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Jan 05 13:27:50 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Jan 05 14:15:37 2012 +0100
@@ -101,13 +101,6 @@
 
   /* specific messages */
 
-  def is_ready(msg: XML.Tree): Boolean =
-    msg match {
-      case XML.Elem(Markup(Isabelle_Markup.STATUS, _),
-        List(XML.Elem(Markup(Isabelle_Markup.READY, _), _))) => true
-      case _ => false
-    }
-
  def is_tracing(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
diff -r f7ee2e5a83dd -r 30a69cd8a9a0 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Jan 05 13:27:50 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Thu Jan 05 14:15:37 2012 +0100
@@ -185,7 +185,7 @@
 
     val _ = Keyword.status ();
     val _ = Thy_Info.status ();
-    val _ = Output.status (Markup.markup Isabelle_Markup.ready "process ready");
+    val _ = Output.raw_message Isabelle_Markup.ready "";
   in loop channel end));
 
 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
diff -r f7ee2e5a83dd -r 30a69cd8a9a0 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Thu Jan 05 13:27:50 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala	Thu Jan 05 14:15:37 2012 +0100
@@ -58,8 +58,7 @@
     def is_status = kind == Isabelle_Markup.STATUS
     def is_report = kind == Isabelle_Markup.REPORT
     def is_raw = kind == Isabelle_Markup.RAW
-    def is_ready = Protocol.is_ready(message)
-    def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr
+    def is_syslog = is_init || is_exit || is_system || is_stderr
 
     override def toString: String =
     {
diff -r f7ee2e5a83dd -r 30a69cd8a9a0 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Jan 05 13:27:50 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Jan 05 14:15:37 2012 +0100
@@ -389,18 +389,17 @@
             val (tag, res) = Invoke_Scala.method(name, arg)
             prover.get.invoke_scala(id, tag, res)
           }
-        case Isabelle_Markup.Cancel_Scala(id) =>
-          System.err.println("cancel_scala " + id)  // FIXME cancel JVM task
+        case Isabelle_Markup.Cancel_Scala(id) if result.is_raw =>
+          System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
+        case Isabelle_Markup.Ready if result.is_raw =>
+            // FIXME move to ML side (!?)
+            syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
+            syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
+            phase = Session.Ready
         case _ =>
           if (result.is_syslog) {
             reverse_syslog ::= result.message
-            if (result.is_ready) {
-              // FIXME move to ML side (!?)
-              syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
-              syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
-              phase = Session.Ready
-            }
-            else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
+            if (result.is_exit && phase == Session.Startup) phase = Session.Failed
             else if (result.is_exit) phase = Session.Inactive
           }
           else if (result.is_stdout) { }