--- a/src/Pure/PIDE/protocol_message.scala Sun Mar 29 13:25:59 2020 +0200
+++ b/src/Pure/PIDE/protocol_message.scala Sun Mar 29 19:42:59 2020 +0200
@@ -9,6 +9,32 @@
object Protocol_Message
{
+ /* message markers */
+
+ object Marker
+ {
+ def apply(a: String): Marker =
+ new Marker { override def name: String = a }
+ }
+
+ abstract class Marker private
+ {
+ def name: String
+ val prefix: String = "\f" + name + " = "
+
+ def apply(text: String): String = prefix + Library.encode_lines(text)
+ def apply(props: Properties.T): String = apply(YXML.string_of_body(XML.Encode.properties(props)))
+
+ def test(line: String): Boolean = line.startsWith(prefix)
+ def test_yxml(line: String): Boolean = test(line) && YXML.detect(line)
+
+ def unapply(line: String): Option[String] =
+ Library.try_unprefix(prefix, line).map(Library.decode_lines)
+
+ override def toString: String = "Marker(" + quote(name) + ")"
+ }
+
+
/* inlined reports */
private val report_elements =