From 7845af3105f1df43dadded4e1ef6f210853c03b3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 27 Jun 2025 14:21:01 +0200 Subject: [PATCH] chore: reserve `public section` syntax (#9032) To be used in the experimental module system --- src/Lean/Elab/BuiltinCommand.lean | 2 +- src/Lean/Parser/Command.lean | 5 +++-- tests/lean/StxQuot.lean.expected.out | 4 ++-- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index d38491942b..198a884aab 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -86,7 +86,7 @@ private def checkEndHeader : Name → List Scope → Option Name @[builtin_command_elab «section»] def elabSection : CommandElab := fun stx => do match stx with - | `($[@[expose%$expTk]]? $[noncomputable%$ncTk]? section $(header?)?) => + | `(Parser.Command.section| $[public%$publicTk]? $[@[expose%$expTk]]? $[noncomputable%$ncTk]? section $(header?)?) => -- TODO: allow more attributes? let attrs ← if expTk.isSome then pure [← `(Parser.Term.attrInstance| expose)] diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 4d7a36ec41..755abd5399 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -246,8 +246,9 @@ def «structure» := leading_parser @[builtin_command_parser] def «deriving» := leading_parser "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover ident skip) ", " def sectionHeader := leading_parser - optional ("@[" >> nonReservedSymbol "expose" >> "]") >> - optional ("noncomputable") + optional ("public ") >> + optional ("@[" >> nonReservedSymbol "expose" >> "] ") >> + optional ("noncomputable ") /-- A `section`/`end` pair delimits the scope of `variable`, `include, `open`, `set_option`, and `local` commands. Sections can be nested. `section ` provides a label to the section that has to appear diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index 4db4a70072..d24c1f4c28 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -34,8 +34,8 @@ StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term "#[(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" (num \"1\")), (Term.matchAlt \"|\" [[(Term.hole \"_\")]] \"=>\" (num \"2\"))]" "(Term.structInst\n \"{\"\n []\n (Term.structInstFields\n [(Term.structInstField\n (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 [])\n [[] [] (Term.structInstFieldDef \":=\" [] `a._@.UnhygienicMain._hyg.1)])])\n (Term.optEllipsis [])\n [\":\" `a._@.UnhygienicMain._hyg.1]\n \"}\")" "(Term.structInst\n \"{\"\n []\n (Term.structInstFields\n [(Term.structInstField\n (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 [])\n [[] [] (Term.structInstFieldDef \":=\" [] `a._@.UnhygienicMain._hyg.1)])])\n (Term.optEllipsis [])\n []\n \"}\")" -"(Command.section (Command.sectionHeader [] []) \"section\" [])" -"(Command.section (Command.sectionHeader [] []) \"section\" [`foo._@.UnhygienicMain._hyg.1])" +"(Command.section (Command.sectionHeader [] [] []) \"section\" [])" +"(Command.section (Command.sectionHeader [] [] []) \"section\" [`foo._@.UnhygienicMain._hyg.1])" "(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [[(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (num \"1\"))]]\n \"=>\"\n («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (num \"1\")))]))" "(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [[(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (num \"1\"))]]\n \"=>\"\n («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (num \"1\")))]))" "#[`a._@.UnhygienicMain._hyg.1, `b._@.UnhygienicMain._hyg.1]"