src/Pure/PIDE/protocol_message.scala
changeset 71623 b3bddebe44ca
parent 71620 5a4ccef7f310
child 71631 3f02bc5a5a03
--- a/src/Pure/PIDE/protocol_message.scala	Sun Mar 29 21:32:20 2020 +0200
+++ b/src/Pure/PIDE/protocol_message.scala	Sun Mar 29 21:57:40 2020 +0200
@@ -15,6 +15,8 @@
   {
     def apply(a: String): Marker =
       new Marker { override def name: String = a }
+
+    def test(line: String): Boolean = line.startsWith("\f")
   }
 
   abstract class Marker private