# HG changeset patch # User wenzelm # Date 1330795119 -3600 # Node ID 38f113b052b1c91473d22c7e2a5af958a91c1f14 # Parent 94259b352ed32a72a182a89eeaa95592f0acb5f9 clarified terminology of raw protocol messages; diff -r 94259b352ed3 -r 38f113b052b1 src/Pure/General/output.ML --- 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; diff -r 94259b352ed3 -r 38f113b052b1 src/Pure/Isar/keyword.ML --- 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) diff -r 94259b352ed3 -r 38f113b052b1 src/Pure/PIDE/isabelle_markup.ML --- 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" diff -r 94259b352ed3 -r 38f113b052b1 src/Pure/PIDE/isabelle_markup.scala --- 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) diff -r 94259b352ed3 -r 38f113b052b1 src/Pure/PIDE/protocol.ML --- 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 _ = diff -r 94259b352ed3 -r 38f113b052b1 src/Pure/System/invoke_scala.ML --- 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); diff -r 94259b352ed3 -r 38f113b052b1 src/Pure/System/isabelle_process.ML --- 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); diff -r 94259b352ed3 -r 38f113b052b1 src/Pure/System/isabelle_process.scala --- 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) diff -r 94259b352ed3 -r 38f113b052b1 src/Pure/System/session.scala --- 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 diff -r 94259b352ed3 -r 38f113b052b1 src/Pure/Thy/thy_info.ML --- 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 *) diff -r 94259b352ed3 -r 38f113b052b1 src/Tools/jEdit/src/protocol_dockable.scala --- 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 } }