From ffbb21a032afba60ad281c5137b602b40ba8f0b7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 16 Jul 2025 13:08:20 +0200
Subject: [PATCH] fix: order of `@[expose] public section`

This PR makes the order of `@[expose] public` at `section` consistent with that at `def`
---
 src/Lean/Elab/BuiltinCommand.lean | 2 +-
 src/Lean/Parser/Command.lean      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index d18429e42a..3081946eb8 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -87,7 +87,7 @@ private def checkEndHeader : Name → List Scope → Option Name
 
 @[builtin_command_elab «section»] def elabSection : CommandElab := fun stx => do
   match stx with
-  | `(Parser.Command.section| $[public%$publicTk]? $[@[expose%$expTk]]? $[noncomputable%$ncTk]? section $(header?)?) =>
+  | `(Parser.Command.section| $[@[expose%$expTk]]? $[public%$publicTk]? $[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 6ee413dc7e..8086a4282b 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -247,8 +247,8 @@ def «structure»          := leading_parser
 @[builtin_command_parser] def «deriving»     := leading_parser
   "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover ident skip) ", "
 def sectionHeader := leading_parser
-  optional ("public ") >>
   optional ("@[" >> nonReservedSymbol "expose" >> "] ") >>
+  optional ("public ") >>
   optional ("noncomputable ")
 /--
 A `section`/`end` pair delimits the scope of `variable`, `include, `open`, `set_option`, and `local`