From 2bdc67756c74d5001013a9f6341f8f1b57e27769 Mon Sep 17 00:00:00 2001
From: "Thomas R. Murrills" <68410468+thorimur@users.noreply.github.com>
Date: Sun, 17 May 2026 13:28:27 -0400
Subject: [PATCH] chore: remove `addInfo` flag from `elabSetOption` (#13736)

This PR removes the `addInfo` flag from `elabSetOption` introduced in
#11313, instead allowing callers to use `withEnableInfoTree` to control
whether infotrees are added.
---
 src/Lean/Elab/SetOption.lean     | 11 +++++------
 src/Lean/Linter/Basic.lean       |  3 ++-
 src/Lean/Linter/MissingDocs.lean |  3 ++-
 3 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Elab/SetOption.lean b/src/Lean/Elab/SetOption.lean
index cfe9ad2283..fd04b63cd2 100644
--- a/src/Lean/Elab/SetOption.lean
+++ b/src/Lean/Elab/SetOption.lean
@@ -49,21 +49,20 @@ where
     | _ => throwUnconfigurable optionName
 
 /--
-Elaborates `id` as an identifier representing an option name with value given by `val`.
+Elaborates `id` as an identifier representing an option name with value given by `val`, adding
+appropriate info to the infotrees.
 
 Validates that `val` has the correct type for values of the option `id`, and returns the updated
 `Options`. Does **not** update the options in the monad `m`.
-
-If `addInfo := true` (the default), adds completion info and elaboration info to the infotrees.
 -/
-def elabSetOption (id : Syntax) (val : Syntax) (addInfo := true) : m (Options × OptionDecl) := do
+def elabSetOption (id : Syntax) (val : Syntax) : m (Options × OptionDecl) := do
   let ref ← getRef
   -- For completion purposes, we discard `val` and any later arguments.
   -- We include the first argument (the keyword) for position information in case `id` is `missing`.
-  if addInfo then addCompletionInfo <| CompletionInfo.option (ref.setArgs (ref.getArgs[*...3]))
+  addCompletionInfo <| CompletionInfo.option (ref.setArgs (ref.getArgs[*...3]))
   let optionName := id.getId.eraseMacroScopes
   let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error ref ex.toString) (getOptionDecl optionName)
-  if addInfo then pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }
+  pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }
   let rec setOption (val : DataValue) : m (Options × OptionDecl) := do
     validateOptionValue optionName decl val
     return ((← getOptions).set optionName val, decl)
diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean
index d186c70359..cf27aeb0eb 100644
--- a/src/Lean/Linter/Basic.lean
+++ b/src/Lean/Linter/Basic.lean
@@ -38,7 +38,8 @@ partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
   if stx.getKind == ``Lean.Parser.Command.in &&
      stx[0].getKind == ``Lean.Parser.Command.set_option then
       -- Do not modify the infotrees when elaborating, and silently ignore errors.
-      let opts ← try (·.1) <$> elabSetOption stx[0][1] stx[0][3] (addInfo := false)
+      let opts ← withEnableInfoTree false try
+          (·.1) <$> elabSetOption stx[0][1] stx[0][3]
         catch _ => getOptions
       withScope ({ · with opts }) do withSetOptionIn cmd stx[2]
   else
diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean
index 5cbf360fe4..5569ff1c2f 100644
--- a/src/Lean/Linter/MissingDocs.lean
+++ b/src/Lean/Linter/MissingDocs.lean
@@ -317,7 +317,8 @@ def handleIn : Handler := fun _ stx => do
   -- `set_option ... in`. This is unlike `withSetOptionIn`, which stops at the first `in` not of
   -- the form `set_option ... in`; as such, we must inline the functionality.
   if stx[0].getKind == ``«set_option» then
-    let opts ← try (·.1) <$> Elab.elabSetOption stx[0][1] stx[0][3] (addInfo := false)
+    let opts ← Elab.withEnableInfoTree false try
+        (·.1) <$> Elab.elabSetOption stx[0][1] stx[0][3]
       catch _ => getOptions
     withScope ({ · with opts }) do missingDocs.run stx[2]
   else