From 7edc42fdfcfbf27580979a864521b3ec0740cd79 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Aug 2021 08:29:30 -0700
Subject: [PATCH] fix: scoped command after `open` command

The issue was reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Ending.20a.20command
---
 src/Lean/Parser/Command.lean               | 10 +++++-----
 tests/lean/run/scopedCommandAfterOpen.lean |  8 ++++++++
 2 files changed, 13 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/scopedCommandAfterOpen.lean

diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 7efa39ff7d..349ca463b6 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -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
diff --git a/tests/lean/run/scopedCommandAfterOpen.lean b/tests/lean/run/scopedCommandAfterOpen.lean
new file mode 100644
index 0000000000..85d8266fdd
--- /dev/null
+++ b/tests/lean/run/scopedCommandAfterOpen.lean
@@ -0,0 +1,8 @@
+namespace Internal
+scoped macro "foo" : command => `(#print "foo")
+end Internal
+
+section
+open Internal
+foo
+end