1.1 --- a/src/Pure/General/output.ML	Sat Mar 03 17:46:50 2012 +0100
     1.2 +++ b/src/Pure/General/output.ML	Sat Mar 03 18:18:39 2012 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4      val prompt_fn: (output -> unit) Unsynchronized.ref
     1.5      val status_fn: (output -> unit) Unsynchronized.ref
     1.6      val report_fn: (output -> unit) Unsynchronized.ref
     1.7 -    val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
     1.8 +    val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
     1.9    end
    1.10    val urgent_message: string -> unit
    1.11    val error_msg': serial * string -> unit
    1.12 @@ -42,7 +42,7 @@
    1.13    val prompt: string -> unit
    1.14    val status: string -> unit
    1.15    val report: string -> unit
    1.16 -  val raw_message: Properties.T -> string -> unit
    1.17 +  val protocol_message: Properties.T -> string -> unit
    1.18  end;
    1.19  
    1.20  structure Output: OUTPUT =
    1.21 @@ -97,8 +97,8 @@
    1.22    val prompt_fn = Unsynchronized.ref physical_stdout;
    1.23    val status_fn = Unsynchronized.ref (fn _: output => ());
    1.24    val report_fn = Unsynchronized.ref (fn _: output => ());
    1.25 -  val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
    1.26 -    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode");
    1.27 +  val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
    1.28 +    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode");
    1.29  end;
    1.30  
    1.31  fun writeln s = ! Private_Hooks.writeln_fn (output s);
    1.32 @@ -110,7 +110,7 @@
    1.33  fun prompt s = ! Private_Hooks.prompt_fn (output s);
    1.34  fun status s = ! Private_Hooks.status_fn (output s);
    1.35  fun report s = ! Private_Hooks.report_fn (output s);
    1.36 -fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s);
    1.37 +fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
    1.38  
    1.39  end;
    1.40  

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

     3.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Sat Mar 03 17:46:50 2012 +0100
     3.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Sat Mar 03 18:18:39 2012 +0100
     3.3 @@ -302,7 +302,7 @@
     3.4  val (badN, bad) = markup_elem "bad";
     3.5  
     3.6  
     3.7 -(* raw message functions *)
     3.8 +(* protocol message functions *)
     3.9  
    3.10  val functionN = "function"
    3.11  

     4.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Sat Mar 03 17:46:50 2012 +0100
     4.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Sat Mar 03 18:18:39 2012 +0100
     4.3 @@ -229,7 +229,7 @@
     4.4    val TRACING = "tracing"
     4.5    val WARNING = "warning"
     4.6    val ERROR = "error"
     4.7 -  val RAW = "raw"
     4.8 +  val PROTOCOL = "protocol"
     4.9    val SYSTEM = "system"
    4.10    val STDOUT = "stdout"
    4.11    val STDERR = "stderr"
    4.12 @@ -242,7 +242,7 @@
    4.13    val BAD = "bad"
    4.14  
    4.15  
    4.16 -  /* raw message functions */
    4.17 +  /* protocol message functions */
    4.18  
    4.19    val FUNCTION = "function"
    4.20    val Function = new Properties.String(FUNCTION)

     5.1 --- a/src/Pure/PIDE/protocol.ML	Sat Mar 03 17:46:50 2012 +0100
     5.2 +++ b/src/Pure/PIDE/protocol.ML	Sat Mar 03 18:18:39 2012 +0100
     5.3 @@ -57,7 +57,7 @@
     5.4          val (assignment, state1) = Document.update old_id new_id edits state;
     5.5          val _ = Future.join_tasks running;
     5.6          val _ =
     5.7 -          Output.raw_message Isabelle_Markup.assign_execs
     5.8 +          Output.protocol_message Isabelle_Markup.assign_execs
     5.9              ((new_id, assignment) |>
    5.10                let open XML.Encode
    5.11                in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
    5.12 @@ -73,7 +73,7 @@
    5.13            YXML.parse_body versions_yxml |>
    5.14              let open XML.Decode in list int end;
    5.15          val state1 = Document.remove_versions versions state;
    5.16 -        val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml;
    5.17 +        val _ = Output.protocol_message Isabelle_Markup.removed_versions versions_yxml;
    5.18        in state1 end));
    5.19  
    5.20  val _ =

     6.1 --- a/src/Pure/System/invoke_scala.ML	Sat Mar 03 17:46:50 2012 +0100
     6.2 +++ b/src/Pure/System/invoke_scala.ML	Sat Mar 03 18:18:39 2012 +0100
     6.3 @@ -33,10 +33,10 @@
     6.4  fun promise_method name arg =
     6.5    let
     6.6      val id = new_id ();
     6.7 -    fun abort () = Output.raw_message (Isabelle_Markup.cancel_scala id) "";
     6.8 +    fun abort () = Output.protocol_message (Isabelle_Markup.cancel_scala id) "";
     6.9      val promise = Future.promise abort : string future;
    6.10      val _ = Synchronized.change promises (Symtab.update (id, promise));
    6.11 -    val _ = Output.raw_message (Isabelle_Markup.invoke_scala name id) arg;
    6.12 +    val _ = Output.protocol_message (Isabelle_Markup.invoke_scala name id) arg;
    6.13    in promise end;
    6.14  
    6.15  fun method name arg = Future.join (promise_method name arg);

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

     8.1 --- a/src/Pure/System/isabelle_process.scala	Sat Mar 03 17:46:50 2012 +0100
     8.2 +++ b/src/Pure/System/isabelle_process.scala	Sat Mar 03 18:18:39 2012 +0100
     8.3 @@ -30,7 +30,7 @@
     8.4        ('E' : Int) -> Isabelle_Markup.TRACING,
     8.5        ('F' : Int) -> Isabelle_Markup.WARNING,
     8.6        ('G' : Int) -> Isabelle_Markup.ERROR,
     8.7 -      ('H' : Int) -> Isabelle_Markup.RAW)
     8.8 +      ('H' : Int) -> Isabelle_Markup.PROTOCOL)
     8.9    }
    8.10  
    8.11    sealed abstract class Message
    8.12 @@ -57,14 +57,14 @@
    8.13      def is_system = kind == Isabelle_Markup.SYSTEM
    8.14      def is_status = kind == Isabelle_Markup.STATUS
    8.15      def is_report = kind == Isabelle_Markup.REPORT
    8.16 -    def is_raw = kind == Isabelle_Markup.RAW
    8.17 +    def is_protocol = kind == Isabelle_Markup.PROTOCOL
    8.18      def is_syslog = is_init || is_exit || is_system || is_stderr
    8.19  
    8.20      override def toString: String =
    8.21      {
    8.22        val res =
    8.23          if (is_status || is_report) message.body.map(_.toString).mkString
    8.24 -        else if (is_raw) "..."
    8.25 +        else if (is_protocol) "..."
    8.26          else Pretty.string_of(message.body)
    8.27        if (properties.isEmpty)
    8.28          kind.toString + " [[" + res + "]]"
    8.29 @@ -96,7 +96,7 @@
    8.30    private def output_message(kind: String, props: Properties.T, body: XML.Body)
    8.31    {
    8.32      if (kind == Isabelle_Markup.INIT) system_channel.accepted()
    8.33 -    if (kind == Isabelle_Markup.RAW)
    8.34 +    if (kind == Isabelle_Markup.PROTOCOL)
    8.35        receiver(new Output(XML.Elem(Markup(kind, props), body)))
    8.36      else {
    8.37        val msg = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
    8.38 @@ -364,7 +364,7 @@
    8.39                case List(XML.Elem(Markup(name, props), Nil))
    8.40                    if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
    8.41                  val kind = Kind.message_markup(name(0))
    8.42 -                val body = read_chunk(kind != Isabelle_Markup.RAW)
    8.43 +                val body = read_chunk(kind != Isabelle_Markup.PROTOCOL)
    8.44                  output_message(kind, props, body)
    8.45                case _ =>
    8.46                  read_chunk(false)

     9.1 --- a/src/Pure/System/session.scala	Sat Mar 03 17:46:50 2012 +0100
     9.2 +++ b/src/Pure/System/session.scala	Sat Mar 03 18:18:39 2012 +0100
     9.3 @@ -58,7 +58,7 @@
     9.4    val phase_changed = new Event_Bus[Session.Phase]
     9.5    val syslog_messages = new Event_Bus[Isabelle_Process.Output]
     9.6    val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
     9.7 -  val protocol_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
     9.8 +  val all_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
     9.9  
    9.10  
    9.11  
    9.12 @@ -200,7 +200,7 @@
    9.13                    val queue1 = queue.enqueue(output.message)
    9.14                    if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
    9.15                  })
    9.16 -            if (output.is_raw) flush()
    9.17 +            if (output.is_protocol) flush()
    9.18            case _ =>
    9.19          }
    9.20        }
    9.21 @@ -356,7 +356,7 @@
    9.22  
    9.23        output.properties match {
    9.24  
    9.25 -        case Position.Id(state_id) if !output.is_raw =>
    9.26 +        case Position.Id(state_id) if !output.is_protocol =>
    9.27            try {
    9.28              val st = global_state >>> (_.accumulate(state_id, output.message))
    9.29              delay_commands_changed.invoke(st.command)
    9.30 @@ -365,7 +365,7 @@
    9.31              case _: Document.State.Fail => bad_output(output)
    9.32            }
    9.33  
    9.34 -        case Isabelle_Markup.Assign_Execs if output.is_raw =>
    9.35 +        case Isabelle_Markup.Assign_Execs if output.is_protocol =>
    9.36            XML.content(output.body).mkString match {
    9.37              case Protocol.Assign(id, assign) =>
    9.38                try { handle_assign(id, assign) }
    9.39 @@ -379,7 +379,7 @@
    9.40              prune_next = System.currentTimeMillis() + prune_delay.ms
    9.41            }
    9.42  
    9.43 -        case Isabelle_Markup.Removed_Versions if output.is_raw =>
    9.44 +        case Isabelle_Markup.Removed_Versions if output.is_protocol =>
    9.45            XML.content(output.body).mkString match {
    9.46              case Protocol.Removed(removed) =>
    9.47                try { handle_removed(removed) }
    9.48 @@ -387,29 +387,29 @@
    9.49              case _ => bad_output(output)
    9.50            }
    9.51  
    9.52 -        case Isabelle_Markup.Invoke_Scala(name, id) if output.is_raw =>
    9.53 +        case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
    9.54            Future.fork {
    9.55              val arg = XML.content(output.body).mkString
    9.56              val (tag, res) = Invoke_Scala.method(name, arg)
    9.57              prover.get.invoke_scala(id, tag, res)
    9.58            }
    9.59  
    9.60 -        case Isabelle_Markup.Cancel_Scala(id) if output.is_raw =>
    9.61 +        case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
    9.62            System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
    9.63  
    9.64 -        case Isabelle_Markup.Ready if output.is_raw =>
    9.65 +        case Isabelle_Markup.Ready if output.is_protocol =>
    9.66              // FIXME move to ML side (!?)
    9.67              syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
    9.68              syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
    9.69              phase = Session.Ready
    9.70  
    9.71 -        case Isabelle_Markup.Loaded_Theory(name) if output.is_raw =>
    9.72 +        case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol =>
    9.73            thy_load.register_thy(name)
    9.74  
    9.75 -        case Isabelle_Markup.Command_Decl(name, kind) if output.is_raw =>
    9.76 +        case Isabelle_Markup.Command_Decl(name, kind) if output.is_protocol =>
    9.77            syntax += (name, kind)
    9.78  
    9.79 -        case Isabelle_Markup.Keyword_Decl(name) if output.is_raw =>
    9.80 +        case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
    9.81            syntax += name
    9.82  
    9.83          case _ =>
    9.84 @@ -471,13 +471,13 @@
    9.85          case Messages(msgs) =>
    9.86            msgs foreach {
    9.87              case input: Isabelle_Process.Input =>
    9.88 -              protocol_messages.event(input)
    9.89 +              all_messages.event(input)
    9.90  
    9.91              case output: Isabelle_Process.Output =>
    9.92                handle_output(output)
    9.93                if (output.is_syslog) syslog_messages.event(output)
    9.94                if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
    9.95 -              protocol_messages.event(output)
    9.96 +              all_messages.event(output)
    9.97            }
    9.98  
    9.99          case change: Change_Node

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

    11.1 --- a/src/Tools/jEdit/src/protocol_dockable.scala	Sat Mar 03 17:46:50 2012 +0100
    11.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Sat Mar 03 18:18:39 2012 +0100
    11.3 @@ -39,6 +39,6 @@
    11.4      }
    11.5    }
    11.6  
    11.7 -  override def init() { Isabelle.session.protocol_messages += main_actor }
    11.8 -  override def exit() { Isabelle.session.protocol_messages -= main_actor }
    11.9 +  override def init() { Isabelle.session.all_messages += main_actor }
   11.10 +  override def exit() { Isabelle.session.all_messages -= main_actor }
   11.11  }