chore: update stage0

stage0/src/Lean/Elab/BuiltinNotation.lean

@@ -96,23 +96,21 @@ are turned into a new anonymous constructor application. For example,
   | _                                                           => Macro.throwUnsupported
 
 open Lean.Parser in
-private def elabParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax := do
+private def elabParserMacroAux (prec : Syntax) (e : Syntax) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do
   let (some declName) ← getDeclName?
     | throwError "invalid `leading_parser` macro, it must be used in definitions"
   match extractMacroScopes declName with
-  | { name := Name.str _ s _, scopes :=  scps, .. } =>
+  | { name := Name.str _ s _, .. } =>
     let kind := quote declName
     let s    := quote s
-    -- if the parser decl is hidden by hygiene, it doesn't make sense to provide an antiquotation kind
-    let antiquotKind ← if scps == [] then `(some $kind) else `(none)
-    ``(withAntiquot (mkAntiquot $s $antiquotKind) (leadingNode $kind $prec $e))
+    ``(withAntiquot (mkAntiquot $s $kind $(quote withAnonymousAntiquot)) (leadingNode $kind $prec $e))
   | _  => throwError "invalid `leading_parser` macro, unexpected declaration name"
 
 @[builtinTermElab «leading_parser»] def elabLeadingParserMacro : TermElab :=
   adaptExpander fun stx => match stx with
-  | `(leading_parser $e)         => elabParserMacroAux (quote Parser.maxPrec) e
-  | `(leading_parser : $prec $e) => elabParserMacroAux prec e
-  | _                            => throwUnsupportedSyntax
+  | `(leading_parser $[: $prec?]? $[(withAnonymousAntiquot := $anon?)]? $e) =>
+    elabParserMacroAux (prec?.getD (quote Parser.maxPrec)) e (anon?.all (·.isOfKind ``Parser.Term.trueVal))
+  | _ => throwUnsupportedSyntax
 
 private def elabTParserMacroAux (prec lhsPrec : Syntax) (e : Syntax) : TermElabM Syntax := do
   let declName? ← getDeclName?

stage0/src/Lean/Elab/Inductive.lean

@@ -705,13 +705,13 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
           Term.ensureNoUnassignedMVars decl
           addDecl decl
           mkAuxConstructions views
-          withSaveInfoContext do  -- save new env
-            for view in views do
-              Term.addTermInfo view.ref[1] (← mkConstWithLevelParams view.declName) (isBinder := true)
-              for ctor in view.ctors do
-                Term.addTermInfo ctor.ref[2] (← mkConstWithLevelParams ctor.declName) (isBinder := true)
-              -- We need to invoke `applyAttributes` because `class` is implemented as an attribute.
-              Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
+    withSaveInfoContext do  -- save new env
+      for view in views do
+        Term.addTermInfo view.ref[1] (← mkConstWithLevelParams view.declName) (isBinder := true)
+        for ctor in view.ctors do
+          Term.addTermInfo ctor.ref[2] (← mkConstWithLevelParams ctor.declName) (isBinder := true)
+        -- We need to invoke `applyAttributes` because `class` is implemented as an attribute.
+        Term.applyAttributesAt view.declName view.modifiers.attrs AttributeApplicationTime.afterTypeChecking
 
 private def applyDerivingHandlers (views : Array InductiveView) : CommandElabM Unit := do
   let mut processed : NameSet := {}

stage0/src/Lean/Parser/Term.lean

@@ -164,7 +164,8 @@ def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun
 @[builtinTermParser] def «fun» := leading_parser:maxPrec ppAllowUngrouped >> unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts)
 
 def optExprPrecedence := optional (atomic ":" >> termParser maxPrec)
-@[builtinTermParser] def «leading_parser»  := leading_parser:leadPrec "leading_parser " >> optExprPrecedence >> termParser
+def withAnonymousAntiquot := leading_parser atomic ("(" >> nonReservedSymbol "withAnonymousAntiquot" >> " := ") >> (trueVal <|> falseVal) >> ")" >> ppSpace
+@[builtinTermParser] def «leading_parser»  := leading_parser:leadPrec "leading_parser " >> optExprPrecedence >> optional withAnonymousAntiquot >> termParser
 @[builtinTermParser] def «trailing_parser» := leading_parser:leadPrec "trailing_parser " >> optExprPrecedence >> optExprPrecedence >> termParser
 
 @[builtinTermParser] def borrowed   := leading_parser "@& " >> termParser leadPrec

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
 #endif
     return opts;
 }