fix: only make the first code action preferred

thorimur · Sep 12, 2023 · 4723c3b · 4723c3b
1 parent a32f7d7
commit 4723c3b
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/Std/Tactic/TryThis.lean b/Std/Tactic/TryThis.lean
@@ -147,14 +147,18 @@ apply the replacement.
     let .ok range := props.getObjValAs? Lsp.Range "range" | panic! "bad type"
     let .ok suggestions := props.getObjVal? "suggestions" | panic! "bad type"
     let .ok suggestions := suggestions.getArr? | panic! "bad type"
-    suggestions.foldlM (init := result) fun result s => do
+    let some s := suggestions[0]? | return result
+    let pushSuggestion (result : Array LazyCodeAction) (s : Json) (isPreferred : Option Bool) := do
       let .ok newText := s.getObjValAs? String "suggestion" | panic! "bad type"
       result.push {
         eager.title := "Try this: " ++ newText
         eager.kind? := "quickfix"
-        eager.isPreferred? := true
+        eager.isPreferred? := isPreferred
         eager.edit? := some <| .ofTextEdit params.textDocument.uri { range, newText }
       }
+    -- Only make the first option preferred
+    let result ← pushSuggestion result s (isPreferred := true)
+    suggestions.foldlM (init := result) (start := 1) (pushSuggestion (isPreferred := none))
 
 /-! # `Suggestion` data -/