clarified terminology of raw protocol messages;

--- a/src/Pure/General/output.ML	Sat Mar 03 17:46:50 2012 +0100
+++ b/src/Pure/General/output.ML	Sat Mar 03 18:18:39 2012 +0100
@@ -34,7 +34,7 @@
     val prompt_fn: (output -> unit) Unsynchronized.ref
     val status_fn: (output -> unit) Unsynchronized.ref
     val report_fn: (output -> unit) Unsynchronized.ref
-    val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
+    val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
   end
   val urgent_message: string -> unit
   val error_msg': serial * string -> unit
@@ -42,7 +42,7 @@
   val prompt: string -> unit
   val status: string -> unit
   val report: string -> unit
-  val raw_message: Properties.T -> string -> unit
+  val protocol_message: Properties.T -> string -> unit
 end;
 
 structure Output: OUTPUT =
@@ -97,8 +97,8 @@
   val prompt_fn = Unsynchronized.ref physical_stdout;
   val status_fn = Unsynchronized.ref (fn _: output => ());
   val report_fn = Unsynchronized.ref (fn _: output => ());
-  val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
-    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode");
+  val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
+    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode");
 end;
 
 fun writeln s = ! Private_Hooks.writeln_fn (output s);
@@ -110,7 +110,7 @@
 fun prompt s = ! Private_Hooks.prompt_fn (output s);
 fun status s = ! Private_Hooks.status_fn (output s);
 fun report s = ! Private_Hooks.report_fn (output s);
-fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s);
+fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
 
 end;
 

--- a/src/Pure/Isar/keyword.ML	Sat Mar 03 17:46:50 2012 +0100
+++ b/src/Pure/Isar/keyword.ML	Sat Mar 03 18:18:39 2012 +0100
@@ -153,7 +153,7 @@
 
 fun status_message m s =
   Position.setmp_thread_data Position.none
-    (if print_mode_active keyword_statusN then Output.raw_message m else writeln) s;
+    (if print_mode_active keyword_statusN then Output.protocol_message m else writeln) s;
 
 fun keyword_status name =
   status_message (Isabelle_Markup.keyword_decl name)

--- a/src/Pure/PIDE/isabelle_markup.ML	Sat Mar 03 17:46:50 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML	Sat Mar 03 18:18:39 2012 +0100
@@ -302,7 +302,7 @@
 val (badN, bad) = markup_elem "bad";
 
 
-(* raw message functions *)
+(* protocol message functions *)
 
 val functionN = "function"
 

--- a/src/Pure/PIDE/isabelle_markup.scala	Sat Mar 03 17:46:50 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala	Sat Mar 03 18:18:39 2012 +0100
@@ -229,7 +229,7 @@
   val TRACING = "tracing"
   val WARNING = "warning"
   val ERROR = "error"
-  val RAW = "raw"
+  val PROTOCOL = "protocol"
   val SYSTEM = "system"
   val STDOUT = "stdout"
   val STDERR = "stderr"
@@ -242,7 +242,7 @@
   val BAD = "bad"
 
 
-  /* raw message functions */
+  /* protocol message functions */
 
   val FUNCTION = "function"
   val Function = new Properties.String(FUNCTION)

--- a/src/Pure/PIDE/protocol.ML	Sat Mar 03 17:46:50 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML	Sat Mar 03 18:18:39 2012 +0100
@@ -57,7 +57,7 @@
         val (assignment, state1) = Document.update old_id new_id edits state;
         val _ = Future.join_tasks running;
         val _ =
-          Output.raw_message Isabelle_Markup.assign_execs
+          Output.protocol_message Isabelle_Markup.assign_execs
             ((new_id, assignment) |>
               let open XML.Encode
               in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
@@ -73,7 +73,7 @@
           YXML.parse_body versions_yxml |>
             let open XML.Decode in list int end;
         val state1 = Document.remove_versions versions state;
-        val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml;
+        val _ = Output.protocol_message Isabelle_Markup.removed_versions versions_yxml;
       in state1 end));
 
 val _ =

--- a/src/Pure/System/invoke_scala.ML	Sat Mar 03 17:46:50 2012 +0100
+++ b/src/Pure/System/invoke_scala.ML	Sat Mar 03 18:18:39 2012 +0100
@@ -33,10 +33,10 @@
 fun promise_method name arg =
   let
     val id = new_id ();
-    fun abort () = Output.raw_message (Isabelle_Markup.cancel_scala id) "";
+    fun abort () = Output.protocol_message (Isabelle_Markup.cancel_scala id) "";
     val promise = Future.promise abort : string future;
     val _ = Synchronized.change promises (Symtab.update (id, promise));
-    val _ = Output.raw_message (Isabelle_Markup.invoke_scala name id) arg;
+    val _ = Output.protocol_message (Isabelle_Markup.invoke_scala name id) arg;
   in promise end;
 
 fun method name arg = Future.join (promise_method name arg);

--- a/src/Pure/System/isabelle_process.ML	Sat Mar 03 17:46:50 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Sat Mar 03 18:18:39 2012 +0100
@@ -109,7 +109,7 @@
     Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
     Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
     Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
-    Output.Private_Hooks.raw_message_fn := message true mbox "H";
+    Output.Private_Hooks.protocol_message_fn := message true mbox "H";
     Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
     Output.Private_Hooks.prompt_fn := ignore;
     message true mbox "A" [] (Session.welcome ())
@@ -185,7 +185,7 @@
 
     val _ = Keyword.status ();
     val _ = Thy_Info.status ();
-    val _ = Output.raw_message Isabelle_Markup.ready "";
+    val _ = Output.protocol_message Isabelle_Markup.ready "";
   in loop channel end));
 
 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);

--- a/src/Pure/System/isabelle_process.scala	Sat Mar 03 17:46:50 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala	Sat Mar 03 18:18:39 2012 +0100
@@ -30,7 +30,7 @@
       ('E' : Int) -> Isabelle_Markup.TRACING,
       ('F' : Int) -> Isabelle_Markup.WARNING,
       ('G' : Int) -> Isabelle_Markup.ERROR,
-      ('H' : Int) -> Isabelle_Markup.RAW)
+      ('H' : Int) -> Isabelle_Markup.PROTOCOL)
   }
 
   sealed abstract class Message
@@ -57,14 +57,14 @@
     def is_system = kind == Isabelle_Markup.SYSTEM
     def is_status = kind == Isabelle_Markup.STATUS
     def is_report = kind == Isabelle_Markup.REPORT
-    def is_raw = kind == Isabelle_Markup.RAW
+    def is_protocol = kind == Isabelle_Markup.PROTOCOL
     def is_syslog = is_init || is_exit || is_system || is_stderr
 
     override def toString: String =
     {
       val res =
         if (is_status || is_report) message.body.map(_.toString).mkString
-        else if (is_raw) "..."
+        else if (is_protocol) "..."
         else Pretty.string_of(message.body)
       if (properties.isEmpty)
         kind.toString + " [[" + res + "]]"
@@ -96,7 +96,7 @@
   private def output_message(kind: String, props: Properties.T, body: XML.Body)
   {
     if (kind == Isabelle_Markup.INIT) system_channel.accepted()
-    if (kind == Isabelle_Markup.RAW)
+    if (kind == Isabelle_Markup.PROTOCOL)
       receiver(new Output(XML.Elem(Markup(kind, props), body)))
     else {
       val msg = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
@@ -364,7 +364,7 @@
               case List(XML.Elem(Markup(name, props), Nil))
                   if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
                 val kind = Kind.message_markup(name(0))
-                val body = read_chunk(kind != Isabelle_Markup.RAW)
+                val body = read_chunk(kind != Isabelle_Markup.PROTOCOL)
                 output_message(kind, props, body)
               case _ =>
                 read_chunk(false)

--- a/src/Pure/System/session.scala	Sat Mar 03 17:46:50 2012 +0100
+++ b/src/Pure/System/session.scala	Sat Mar 03 18:18:39 2012 +0100
@@ -58,7 +58,7 @@
   val phase_changed = new Event_Bus[Session.Phase]
   val syslog_messages = new Event_Bus[Isabelle_Process.Output]
   val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
-  val protocol_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
+  val all_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
 
 
 
@@ -200,7 +200,7 @@
                   val queue1 = queue.enqueue(output.message)
                   if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
                 })
-            if (output.is_raw) flush()
+            if (output.is_protocol) flush()
           case _ =>
         }
       }
@@ -356,7 +356,7 @@
 
       output.properties match {
 
-        case Position.Id(state_id) if !output.is_raw =>
+        case Position.Id(state_id) if !output.is_protocol =>
           try {
             val st = global_state >>> (_.accumulate(state_id, output.message))
             delay_commands_changed.invoke(st.command)
@@ -365,7 +365,7 @@
             case _: Document.State.Fail => bad_output(output)
           }
 
-        case Isabelle_Markup.Assign_Execs if output.is_raw =>
+        case Isabelle_Markup.Assign_Execs if output.is_protocol =>
           XML.content(output.body).mkString match {
             case Protocol.Assign(id, assign) =>
               try { handle_assign(id, assign) }
@@ -379,7 +379,7 @@
             prune_next = System.currentTimeMillis() + prune_delay.ms
           }
 
-        case Isabelle_Markup.Removed_Versions if output.is_raw =>
+        case Isabelle_Markup.Removed_Versions if output.is_protocol =>
           XML.content(output.body).mkString match {
             case Protocol.Removed(removed) =>
               try { handle_removed(removed) }
@@ -387,29 +387,29 @@
             case _ => bad_output(output)
           }
 
-        case Isabelle_Markup.Invoke_Scala(name, id) if output.is_raw =>
+        case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
           Future.fork {
             val arg = XML.content(output.body).mkString
             val (tag, res) = Invoke_Scala.method(name, arg)
             prover.get.invoke_scala(id, tag, res)
           }
 
-        case Isabelle_Markup.Cancel_Scala(id) if output.is_raw =>
+        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_raw =>
+        case Isabelle_Markup.Ready if output.is_protocol =>
             // 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 Isabelle_Markup.Loaded_Theory(name) if output.is_raw =>
+        case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol =>
           thy_load.register_thy(name)
 
-        case Isabelle_Markup.Command_Decl(name, kind) if output.is_raw =>
+        case Isabelle_Markup.Command_Decl(name, kind) if output.is_protocol =>
           syntax += (name, kind)
 
-        case Isabelle_Markup.Keyword_Decl(name) if output.is_raw =>
+        case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
           syntax += name
 
         case _ =>
@@ -471,13 +471,13 @@
         case Messages(msgs) =>
           msgs foreach {
             case input: Isabelle_Process.Input =>
-              protocol_messages.event(input)
+              all_messages.event(input)
 
             case output: Isabelle_Process.Output =>
               handle_output(output)
               if (output.is_syslog) syslog_messages.event(output)
               if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
-              protocol_messages.event(output)
+              all_messages.event(output)
           }
 
         case change: Change_Node

--- a/src/Pure/Thy/thy_info.ML	Sat Mar 03 17:46:50 2012 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Mar 03 18:18:39 2012 +0100
@@ -89,7 +89,8 @@
 fun get_names () = Graph.topological_order (get_thys ());
 
 fun status () =
-  List.app (fn name => Output.raw_message (Isabelle_Markup.loaded_theory name) "") (get_names ());
+  List.app (fn name => Output.protocol_message (Isabelle_Markup.loaded_theory name) "")
+    (get_names ());
 
 
 (* access thy *)

--- a/src/Tools/jEdit/src/protocol_dockable.scala	Sat Mar 03 17:46:50 2012 +0100
+++ b/src/Tools/jEdit/src/protocol_dockable.scala	Sat Mar 03 18:18:39 2012 +0100
@@ -39,6 +39,6 @@
     }
   }
 
-  override def init() { Isabelle.session.protocol_messages += main_actor }
-  override def exit() { Isabelle.session.protocol_messages -= main_actor }
+  override def init() { Isabelle.session.all_messages += main_actor }
+  override def exit() { Isabelle.session.all_messages -= main_actor }
 }