From 392d078011976150d8d8a8b5040acf4aee1bf134 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Jun 2020 10:31:13 -0700
Subject: [PATCH] feat: declare quotation parser for new parsing category

@Kha We can now delete the command
```
@[termParser] def childStxQuot : Parser :=
checkPrec maxPrec >> (node `Lean.Parser.Term.stxQuot $ symbol "`(child|" >> categoryParser `child 0 >> symbol ")")
```
from the web demo.
---
 src/Lean/Elab/Syntax.lean | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 8d73800398..f21f275203 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -154,13 +154,24 @@ end Term
 
 namespace Command
 
+private def getCatSuffix (catName : Name) : String :=
+match catName with
+| Name.str _ s _ => s
+| _              => unreachable!
+
+private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
+let quotSymbol := "`(" ++ getCatSuffix catName ++ "|";
+cmd ← `(@[termParser] def catStxQuot : Lean.ParserDescr := Lean.ParserDescr.node `Lean.Parser.Term.stxQuot $(quote Lean.Parser.maxPrec) (Lean.ParserDescr.andthen (Lean.ParserDescr.symbol $(quote quotSymbol)) (Lean.ParserDescr.andthen (Lean.ParserDescr.parser $(quote catName) 0) (Lean.ParserDescr.symbol ")"))));
+elabCommand cmd
+
 @[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab :=
 fun stx => do
   let catName  := stx.getIdAt 1;
   let attrName := catName.appendAfter "Parser";
   env ← getEnv;
   env ← liftIO stx $ Parser.registerParserCategory env attrName catName;
-  setEnv env
+  setEnv env;
+  declareSyntaxCatQuotParser catName
 
 def mkKindName (catName : Name) : Name :=
 `_kind ++ catName