From 642850efb236e3f67e76b5f39bb9f8a88c07096f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 22 Jan 2020 11:51:51 -0800
Subject: [PATCH] fix: antiquotation for all categories

---
 src/Init/Lean/Parser/Parser.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index c8961a8d3b..8735fb1dc6 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1755,13 +1755,20 @@ match (parserExtension.getState env).categories.find? catName with
 | none     => false
 | some cat => cat.leadingIdentAsSymbol
 
-def categoryParserFnImpl (catName : Name) : ParserFn leading :=
+def categoryParserFnImplAux (catName : Name) : ParserFn leading :=
 fun rbp ctx s =>
   let categories := (parserExtension.getState ctx.env).categories;
   match categories.find? catName with
   | some cat => prattParser catName cat.tables cat.leadingIdentAsSymbol rbp ctx s
   | none     => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'")
 
+private def catNameToString : Name → String
+| Name.str Name.anonymous s _ => s
+| n                           => n.toString
+
+def categoryParserFnImpl (catName : Name) : ParserFn leading :=
+orelseFn (mkAntiquot (catNameToString catName) none false).fn (categoryParserFnImplAux catName)
+
 @[init] def setCategoryParserFnRef : IO Unit :=
 categoryParserFnRef.set categoryParserFnImpl