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