fix: use two tokens for open private/export private (#1050)

Batteries/Tactic/OpenPrivate.lean

@@ -99,7 +99,7 @@ name component.
 It is also possible to specify the module instead with
 `open private a b c from Other.Module`.
 -/
-syntax (name := openPrivate) "open private" (ppSpace ident)*
+syntax (name := openPrivate) "open" ppSpace "private" (ppSpace ident)*
   (" in" (ppSpace ident)*)? (" from" (ppSpace ident)*)? : command
 
 /-- Elaborator for `open private`. -/
@@ -119,7 +119,7 @@ It will also open the newly created alias definition under the provided short na
 It is also possible to specify the module instead with
 `export private a b c from Other.Module`.
 -/
-syntax (name := exportPrivate) "export private" (ppSpace ident)*
+syntax (name := exportPrivate) "export" ppSpace "private" (ppSpace ident)*
   (" in" (ppSpace ident)*)? (" from" (ppSpace ident)*)? : command
 
 /-- Elaborator for `export private`. -/

BatteriesTest/OpenPrivateDefs.lean

@@ -0,0 +1,4 @@
+/-!
+This file contains a private declaration. It's tested in `openPrivate.lean`.
+-/
+private def secretNumber : Nat := 2

BatteriesTest/openPrivate.lean

@@ -0,0 +1,37 @@
+
+import Batteries.Tactic.OpenPrivate
+
+import BatteriesTest.OpenPrivateDefs
+
+
+
+/-- error: unknown identifier 'secretNumber' -/
+#guard_msgs in
+#eval secretNumber
+
+
+-- It works with one space between the tokens
+/-- info: 2 -/
+#guard_msgs in
+open private secretNumber from BatteriesTest.OpenPrivateDefs in
+#eval secretNumber
+
+
+-- It also works with other kinds of whitespace between the tokens
+
+/-- info: 2 -/
+#guard_msgs in
+open      private secretNumber from BatteriesTest.OpenPrivateDefs in
+#eval secretNumber
+
+
+/-- info: 2 -/
+#guard_msgs in
+open
+  private secretNumber from BatteriesTest.OpenPrivateDefs in
+#eval secretNumber
+
+/-- info: 2 -/
+#guard_msgs in
+open /- Being sneaky! -/ private secretNumber from BatteriesTest.OpenPrivateDefs in
+#eval secretNumber