From d7e14ba47f11a3cf2e76dde5d5d188eca77581f7 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 7 Aug 2022 15:11:07 +0200 Subject: [PATCH] feat: `openDecl` antiquotation --- src/Lean/Parser/Command.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 6f52e4ec62..6448faf59d 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -143,7 +143,8 @@ def openRenaming := leading_parser atomic (ident >> "renaming") >> sepBy1 op def openOnly := leading_parser atomic (ident >> " (") >> many1 ident >> ")" def openSimple := leading_parser many1 (checkColGt >> ident) def openScoped := leading_parser "scoped " >> many1 (checkColGt >> ident) -def openDecl := openHiding <|> openRenaming <|> openOnly <|> openSimple <|> openScoped +def openDecl := withAntiquot (mkAntiquot "openDecl" `Lean.Parser.Command.openDecl (isPseudoKind := true)) <| + openHiding <|> openRenaming <|> openOnly <|> openSimple <|> openScoped @[builtinCommandParser] def «open» := leading_parser withPosition ("open " >> openDecl) @[builtinCommandParser] def «mutual» := leading_parser "mutual " >> many1 (ppLine >> notSymbol "end" >> commandParser) >> ppDedent (ppLine >> "end") >> terminationSuffix