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

@@ -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)]

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`