# HG changeset patch # User wenzelm # Date 1671375697 -3600 # Node ID e95b9c9e17ff7ad8b7db57b5c4a2a81ca979a49c # Parent fdaa17402af32d97779d3fef23f7af1de8ede6a7 clarified signature; diff -r fdaa17402af3 -r e95b9c9e17ff src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sun Dec 18 15:50:51 2022 +0100 +++ b/src/Pure/PIDE/command.scala Sun Dec 18 16:01:37 2022 +0100 @@ -340,7 +340,7 @@ props match { case Markup.Serial(i) => val markup_message = - cache.elem(Protocol.make_message(body, kind = name, props = props)) + cache.elem(Protocol.make_message(body, name, props = props)) val message_markup = cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL)))) diff -r fdaa17402af3 -r e95b9c9e17ff src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Sun Dec 18 15:50:51 2022 +0100 +++ b/src/Pure/PIDE/protocol.scala Sun Dec 18 16:01:37 2022 +0100 @@ -202,13 +202,16 @@ text1 + text2 } - def make_message(body: XML.Body, - kind: String = Markup.WRITELN, - props: Properties.T = Nil - ): XML.Elem = XML.Elem(Markup(Markup.message(kind), props), body) + def make_message(body: XML.Body, kind: String, props: Properties.T = Nil): XML.Elem = + XML.Elem(Markup(Markup.message(kind), props), body) - def warning_message(body: XML.Body): XML.Elem = make_message(body, kind = Markup.WARNING) - def error_message(body: XML.Body): XML.Elem = make_message(body, kind = Markup.ERROR) + def writeln_message(body: XML.Body): XML.Elem = make_message(body, Markup.WRITELN) + def warning_message(body: XML.Body): XML.Elem = make_message(body, Markup.WARNING) + def error_message(body: XML.Body): XML.Elem = make_message(body, Markup.ERROR) + + def writeln_message(msg: String): XML.Elem = writeln_message(XML.string(msg)) + def warning_message(msg: String): XML.Elem = warning_message(XML.string(msg)) + def error_message(msg: String): XML.Elem = error_message(XML.string(msg)) /* ML profiling */ diff -r fdaa17402af3 -r e95b9c9e17ff src/Pure/PIDE/query_operation.scala --- a/src/Pure/PIDE/query_operation.scala Sun Dec 18 15:50:51 2022 +0100 +++ b/src/Pure/PIDE/query_operation.scala Sun Dec 18 16:01:37 2022 +0100 @@ -119,7 +119,7 @@ XML.Elem(_, List(XML.Elem(markup, body))) <- results if Markup.messages.contains(markup.name) body1 = resolve_sendback(body) - } yield Protocol.make_message(body1, kind = markup.name, props = markup.properties) + } yield Protocol.make_message(body1, markup.name, props = markup.properties) /* status */ diff -r fdaa17402af3 -r e95b9c9e17ff src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala Sun Dec 18 15:50:51 2022 +0100 +++ b/src/Pure/Tools/debugger.scala Sun Dec 18 16:01:37 2022 +0100 @@ -123,7 +123,7 @@ case Markup.Debugger_Output(thread_name) => Symbol.decode_yxml_failsafe(msg.text) match { case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) => - val message = Protocol.make_message(body, kind = name, props = props) + val message = Protocol.make_message(body, name, props = props) debugger.add_output(thread_name, i -> session.cache.elem(message)) true case _ => false diff -r fdaa17402af3 -r e95b9c9e17ff src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Sun Dec 18 15:50:51 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Sun Dec 18 16:01:37 2022 +0100 @@ -142,8 +142,8 @@ } val msg = res match { - case Exn.Res(_) => Protocol.make_message(XML.string("OK")) - case Exn.Exn(exn) => Protocol.error_message(XML.string(Exn.message(exn))) + case Exn.Res(_) => Protocol.writeln_message("OK") + case Exn.Exn(exn) => Protocol.error_message(Exn.message(exn)) } val result = Document_Dockable.Result(output = List(msg)) current_state.change(_ => Document_Dockable.State.finish(result))