src/Pure/Isar/parse.scala

--- a/src/Pure/Isar/parse.scala	Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/Isar/parse.scala	Sun Mar 10 00:21:34 2019 +0100
@@ -80,7 +80,13 @@
           tok.kind == Token.Kind.IDENT ||
           tok.kind == Token.Kind.STRING)
 
-    def tags: Parser[List[String]] = rep($$$("%") ~> tag_name)
+    def tag: Parser[String] = $$$("%") ~> tag_name
+    def tags: Parser[List[String]] = rep(tag)
+
+    def marker: Parser[String] =
+      ($$$(Symbol.marker) | $$$(Symbol.marker_decoded)) ~! embedded ^^ { case _ ~ x => x }
+
+    def annotation: Parser[Unit] = rep(marker | tag) ^^ { case _ => () }
 
 
     /* wrappers */