From 182270f8bfc6ce00e83837e790effaff2fe594d7 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Sat, 6 Apr 2024 14:00:34 -0400
Subject: [PATCH] fix: typo in `withSetOptionIn` (#3806)

When using `withSetOptionIn` on syntax `set_option ... in <command>`,
recurse into command syntax (`stx[2]`) instead of the syntax `in`
(`stx[1]`).

---

Demonstration of `stx[1]` vs. `stx[2]`:
```lean
import Lean

def stx := (Lean.Unhygienic.run `(set_option trace.debug true in #print foo)).raw

#eval stx[1] -- Lean.Syntax.atom (Lean.SourceInfo.none) "in"
#eval stx[2] -- `#print` command syntax
```
---
 src/Lean/Elab/Command.lean                   |  2 +-
 tests/lean/withSetOptionIn.lean              | 39 ++++++++++++++++++++
 tests/lean/withSetOptionIn.lean.expected.out |  0
 3 files changed, 40 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/withSetOptionIn.lean
 create mode 100644 tests/lean/withSetOptionIn.lean.expected.out

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 758c25ffaf..cebd8e4c00 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -537,7 +537,7 @@ partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
      stx[0].getKind == ``Lean.Parser.Command.set_option then
       let opts ← Elab.elabSetOption stx[0][1] stx[0][3]
       Command.withScope (fun scope => { scope with opts }) do
-        withSetOptionIn cmd stx[1]
+        withSetOptionIn cmd stx[2]
   else
     cmd stx
 
diff --git a/tests/lean/withSetOptionIn.lean b/tests/lean/withSetOptionIn.lean
new file mode 100644
index 0000000000..8f34667133
--- /dev/null
+++ b/tests/lean/withSetOptionIn.lean
@@ -0,0 +1,39 @@
+import Lean
+
+/-!
+# `withSetOptionIn`
+
+This test checks that `withSetOptionIn` recurses into the command syntax (`stx[2]`) in
+`set_option ... in <cmd>`.
+
+Prior to #3806, `withSetOptionIn` erroneously recursed into the syntax `in` (`stx[1]`).
+-/
+
+open Lean Elab Command
+
+/-- Trace `foo` when `set_option trace.debug true`. -/
+elab "#trace_debug_foo" : command => do trace[debug] "foo"
+
+/-- Elab `cmd` using `withSetOptionIn`. -/
+elab "#test " cmd:command : command => withSetOptionIn elabCommand cmd
+
+/-! ## Controls
+
+Ensure that `#trace_debug_foo` works as expected.
+-/
+
+#guard_msgs in
+#trace_debug_foo
+
+/-- info: [debug] foo -/
+#guard_msgs in
+set_option trace.debug true in #trace_debug_foo
+
+/-! ## Test
+
+Should trace `[debug] foo`, and not log the error "unexpected command 'in'".
+-/
+
+/-- info: [debug] foo -/
+#guard_msgs in
+#test set_option trace.debug true in #trace_debug_foo
diff --git a/tests/lean/withSetOptionIn.lean.expected.out b/tests/lean/withSetOptionIn.lean.expected.out
new file mode 100644
index 0000000000..e69de29bb2