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

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

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

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