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