max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: whitespace around parens in open/export

Browse source
This commit is contained in:
Gabriel Ebner 2021-12-09 14:34:47 +01:00 • committed by Sebastian Ullrich
parent 87faa7a93a
commit 52b36cad1d
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Parser/Command.lean
View file

@ -113,11 +113,11 @@ def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> st
@[builtinCommandParser] def «set_option» := leading_parser "set_option " >> ident >> ppSpace >> optionValue
def eraseAttr := leading_parser "-" >> rawIdent
@[builtinCommandParser] def «attribute» := leading_parser "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "] " >> many1 ident
@[builtinCommandParser] def «export» := leading_parser "export " >> ident >> "(" >> many1 ident >> ")"
@[builtinCommandParser] def «export» := leading_parser "export " >> ident >> " (" >> many1 ident >> ")"
def openHiding := leading_parser atomic (ident >> "hiding") >> many1 (checkColGt >> ident)
def openRenamingItem := leading_parser ident >> unicodeSymbol "→" "->" >> checkColGt >> ident
def openRenamingItem := leading_parser ident >> unicodeSymbol " → " " -> " >> checkColGt >> ident
def openRenaming := leading_parser atomic (ident >> "renaming") >> sepBy1 openRenamingItem ", "
def openOnly := leading_parser atomic (ident >> "(") >> many1 ident >> ")"
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