From 01f4969b6e861db6a99261ea5eadd5a9bb63011b Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 15 Nov 2024 08:55:10 +0100 Subject: [PATCH] fix: use two tokens for open private/export private (#1050) --- Batteries/Tactic/OpenPrivate.lean | 4 ++-- BatteriesTest/OpenPrivateDefs.lean | 4 ++++ BatteriesTest/openPrivate.lean | 37 ++++++++++++++++++++++++++++++ 3 files changed, 43 insertions(+), 2 deletions(-) create mode 100644 BatteriesTest/OpenPrivateDefs.lean create mode 100644 BatteriesTest/openPrivate.lean diff --git a/Batteries/Tactic/OpenPrivate.lean b/Batteries/Tactic/OpenPrivate.lean index 7ade0b94d9..a7e126133f 100644 --- a/Batteries/Tactic/OpenPrivate.lean +++ b/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`. -/ diff --git a/BatteriesTest/OpenPrivateDefs.lean b/BatteriesTest/OpenPrivateDefs.lean new file mode 100644 index 0000000000..f5d1a483e4 --- /dev/null +++ b/BatteriesTest/OpenPrivateDefs.lean @@ -0,0 +1,4 @@ +/-! +This file contains a private declaration. It's tested in `openPrivate.lean`. +-/ +private def secretNumber : Nat := 2 diff --git a/BatteriesTest/openPrivate.lean b/BatteriesTest/openPrivate.lean new file mode 100644 index 0000000000..36f042c634 --- /dev/null +++ b/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