# HG changeset patch
# User wenzelm
# Date 1325771321 -3600
# Node ID aa5c367ee579c39d56fb7f2e4308510c2eb27f42
# Parent  1e9ec1a44dfcf3667e83b1fb025cea43f17fe257
prefer raw_message for protocol implementation;

diff -r 1e9ec1a44dfc -r aa5c367ee579 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Thu Jan 05 14:34:18 2012 +0100
+++ b/src/Pure/Isar/keyword.ML	Thu Jan 05 14:48:41 2012 +0100
@@ -151,17 +151,17 @@
 
 val keyword_statusN = "keyword_status";
 
-fun status_message s =
+fun status_message m s =
   Position.setmp_thread_data Position.none
-    (if print_mode_active keyword_statusN then Output.status else writeln) s;
+    (if print_mode_active keyword_statusN then Output.raw_message m else writeln) s;
 
 fun keyword_status name =
-  status_message (Markup.markup (Isabelle_Markup.keyword_decl name)
-    ("Outer syntax keyword: " ^ quote name));
+  status_message (Isabelle_Markup.keyword_decl name)
+    ("Outer syntax keyword: " ^ quote name);
 
 fun command_status (name, kind) =
-  status_message (Markup.markup (Isabelle_Markup.command_decl name (kind_of kind))
-    ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
+  status_message (Isabelle_Markup.command_decl name (kind_of kind))
+    ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")");
 
 fun status () =
   let val (keywords, commands) = CRITICAL (fn () =>
diff -r 1e9ec1a44dfc -r aa5c367ee579 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Thu Jan 05 14:34:18 2012 +0100
+++ b/src/Pure/Isar/keyword.scala	Thu Jan 05 14:48:41 2012 +0100
@@ -54,26 +54,5 @@
     Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
   val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
   val improper = Set(THY_SCRIPT, PRF_SCRIPT)
-
-
-  /* protocol messages */
-
-  object Keyword_Decl {
-    def unapply(msg: XML.Tree): Option[String] =
-      msg match {
-        case XML.Elem(Markup(Isabelle_Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) =>
-          Some(name)
-        case _ => None
-      }
-  }
-
-  object Command_Decl {
-    def unapply(msg: XML.Tree): Option[(String, String)] =
-      msg match {
-        case XML.Elem(Markup(Isabelle_Markup.COMMAND_DECL,
-            List((Markup.NAME, name), (Markup.KIND, kind))), _) => Some((name, kind))
-        case _ => None
-      }
-  }
 }
 
diff -r 1e9ec1a44dfc -r aa5c367ee579 src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Thu Jan 05 14:34:18 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML	Thu Jan 05 14:48:41 2012 +0100
@@ -66,8 +66,6 @@
   val ML_antiquotationN: string
   val doc_antiquotationN: string
   val doc_antiquotation_optionN: string
-  val keyword_declN: string val keyword_decl: string -> Markup.T
-  val command_declN: string val command_decl: string -> string -> Markup.T
   val keywordN: string val keyword: Markup.T
   val operatorN: string val operator: Markup.T
   val commandN: string val command: Markup.T
@@ -105,6 +103,8 @@
   val functionN: string
   val ready: Properties.T
   val loaded_theory: string -> Properties.T
+  val keyword_decl: string -> Properties.T
+  val command_decl: string -> string -> Properties.T
   val assign_execs: Properties.T
   val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
@@ -235,13 +235,6 @@
 
 (* outer syntax *)
 
-val (keyword_declN, keyword_decl) = markup_string "keyword_decl" Markup.nameN;
-
-val command_declN = "command_decl";
-
-fun command_decl name kind : Markup.T =
-  (command_declN, [(Markup.nameN, name), (Markup.kindN, kind)]);
-
 val (keywordN, keyword) = markup_elem "keyword";
 val (operatorN, operator) = markup_elem "operator";
 val (commandN, command) = markup_elem "command";
@@ -317,6 +310,10 @@
 
 fun loaded_theory name = [(functionN, "loaded_theory"), (Markup.nameN, name)];
 
+fun keyword_decl name = [(functionN, "keyword_decl"), (Markup.nameN, name)];
+fun command_decl name kind =
+  [(functionN, "command_decl"), (Markup.nameN, name), (Markup.kindN, kind)];
+
 val assign_execs = [(functionN, "assign_execs")];
 val removed_versions = [(functionN, "removed_versions")];
 
diff -r 1e9ec1a44dfc -r aa5c367ee579 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Thu Jan 05 14:34:18 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala	Thu Jan 05 14:48:41 2012 +0100
@@ -142,9 +142,6 @@
 
   /* outer syntax */
 
-  val KEYWORD_DECL = "keyword_decl"
-  val COMMAND_DECL = "command_decl"
-
   val KEYWORD = "keyword"
   val OPERATOR = "operator"
   val COMMAND = "command"
@@ -261,6 +258,24 @@
       }
   }
 
+  object Keyword_Decl
+  {
+    def unapply(props: Properties.T): Option[String] =
+      props match {
+        case List((FUNCTION, "keyword_decl"), (Markup.NAME, name)) => Some(name)
+        case _ => None
+      }
+  }
+  object Command_Decl
+  {
+    def unapply(props: Properties.T): Option[(String, String)] =
+      props match {
+        case List((FUNCTION, "command_decl"), (Markup.NAME, name), (Markup.KIND, kind)) =>
+          Some((name, kind))
+        case _ => None
+      }
+  }
+
   val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
   val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
 
diff -r 1e9ec1a44dfc -r aa5c367ee579 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Jan 05 14:34:18 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Jan 05 14:48:41 2012 +0100
@@ -406,6 +406,12 @@
         case Isabelle_Markup.Loaded_Theory(name) if result.is_raw =>
           thy_load.register_thy(name)
 
+        case Isabelle_Markup.Command_Decl(name, kind) if result.is_raw =>
+          syntax += (name, kind)
+
+        case Isabelle_Markup.Keyword_Decl(name) if result.is_raw =>
+          syntax += name
+
         case _ =>
           if (result.is_syslog) {
             reverse_syslog ::= result.message
@@ -413,13 +419,6 @@
             else if (result.is_exit) phase = Session.Inactive
           }
           else if (result.is_stdout) { }
-          else if (result.is_status) {
-            result.body match {
-              case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
-              case List(Keyword.Keyword_Decl(name)) => syntax += name
-              case _ => bad_result(result)
-            }
-          }
           else bad_result(result)
       }
     }