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

fix: scoped command after open command

Browse source 
The issue was reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Ending.20a.20command
This commit is contained in:
Leonardo de Moura 2021-08-23 08:29:30 -07:00
parent 5a7044365b
commit 7edc42fdfc
2 changed files with 13 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -89,14 +89,14 @@ def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> st
def eraseAttr := leading_parser "-" >> ident
@[builtinCommandParser] def «attribute» := leading_parser "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "] " >> many1 ident
@[builtinCommandParser] def «export» := leading_parser "export " >> ident >> "(" >> many1 ident >> ")"
def openHiding := leading_parser atomic (ident >> "hiding") >> many1 ident
def openRenamingItem := leading_parser ident >> unicodeSymbol "→" "->" >> ident
def openHiding := leading_parser atomic (ident >> "hiding") >> many1 (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 openSimple := leading_parser many1 ident
def openScoped := leading_parser "scoped " >> many1 ident
def openSimple := leading_parser many1 (checkColGt >> ident)
def openScoped := leading_parser "scoped " >> many1 (checkColGt >> ident)
def openDecl := openHiding <|> openRenaming <|> openOnly <|> openSimple <|> openScoped
@[builtinCommandParser] def «open» := leading_parser "open " >> openDecl
@[builtinCommandParser] def «open» := leading_parser withPosition ("open " >> openDecl)
@[builtinCommandParser] def «mutual» := leading_parser "mutual " >> many1 (ppLine >> notSymbol "end" >> commandParser) >> ppDedent (ppLine >> "end")
@[builtinCommandParser] def «initialize» := leading_parser optional visibility >> "initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq

8
tests/lean/run/scopedCommandAfterOpen.lean Normal file
View file

@ -0,0 +1,8 @@
namespace Internal
scoped macro "foo" : command => `(#print "foo")
end Internal
section
open Internal
foo
end