feat: add markMeta parameter to addAndCompile (#13311)

This PR adds an optional `markMeta : Bool := false` parameter to
`addAndCompile`, so that callers can propagate the `meta` marking
without manually splitting into `addDecl` + `markMeta` + `compileDecl`.

Also updates `ParserCompiler` to use the new parameter.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

src/Lean/AddDecl.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Sorry
 public import Lean.Util.CollectAxioms
 public import Lean.OriginalConstKind
+import Lean.Compiler.MetaAttr
 import all Lean.OriginalConstKind  -- for accessing `privateConstKindsExt`
 
 public section
@@ -208,8 +209,12 @@ where
       catch _ => pure ()
 
 
-def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true) : CoreM Unit := do
+def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true)
+    (markMeta : Bool := false) : CoreM Unit := do
   addDecl decl
+  if markMeta then
+    for n in decl.getNames do
+      modifyEnv (Lean.markMeta · n)
   compileDecl decl (logErrors := logCompileErrors)
 
 end Lean

src/Lean/ParserCompiler.lean

@@ -110,9 +110,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
         }
         -- usually `meta` is inferred during compilation for auxiliary definitions, but as
         -- `ctx.combinatorAttr` may enforce correct use of the modifier, infer now.
-        if isMarkedMeta (← getEnv) c then
-          modifyEnv (markMeta · c')
-        addAndCompile decl
+        addAndCompile decl (markMeta := isMarkedMeta (← getEnv) c)
         modifyEnv (ctx.combinatorAttr.setDeclFor · c c')
         if cinfo.type.isConst then
           if let some kind ← parserNodeKind? cinfo.value! then