tuned;
authorwenzelm
Sat, 10 Dec 2022 15:57:21 +0100
changeset 76613 b945e30b7471
parent 76612 2436f9c43b2d
child 76614 ac08b6e3b9e3
tuned;
src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Fri Dec 09 15:53:09 2022 +0100
+++ b/src/Pure/Isar/parse.scala	Sat Dec 10 15:57:21 2022 +0100
@@ -66,7 +66,7 @@
     def document_source: Parser[String] = atom("document source", _.is_embedded)
 
     def opt_keyword(s: String): Parser[Boolean] =
-      ($$$("(") ~! $$$(s) ~ $$$(")")) ^^ { case _ => true } | success(false)
+      ($$$("(") ~! $$$(s) ~ $$$(")")) ^^ (_ => true) | success(false)
 
     def path: Parser[String] =
       atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content))
@@ -85,7 +85,7 @@
 
     def marker: Parser[String] = token("marker", _.is_marker) ^^ (_.content)
 
-    def annotation: Parser[Unit] = rep(tag | marker) ^^ { case _ => () }
+    def annotation: Parser[Unit] = rep(tag | marker) ^^ (_ => ())
 
 
     /* wrappers */
@@ -100,4 +100,3 @@
     }
   }
 }
-