feat: allow extracting try this suggestions from infotree

Author: mhuisi

src/Lean/Meta/Hint.lean

@@ -432,12 +432,21 @@ def mkSuggestionsMessage (suggestions : Array Suggestion) (ref : Syntax)
   for suggestion in suggestions do
     let some range := suggestion.span?.getD ref |>.getRange?
       | continue
-    let { info, suggestions := suggestionArr, range := lspRange } ←
-      processSuggestions ref range #[suggestion.toTryThisSuggestion] codeActionPrefix?
+    let edit ← suggestion.processEdit range
+    let suggestionText := edit.newText
+    let ref := Syntax.ofRange <| ref.getRange?.getD range
+    let codeActionTitleOverride? := suggestion.toCodeActionTitle?.map (· suggestionText)
+    let codeActionTitle := codeActionTitleOverride?.getD <| (codeActionPrefix?.getD "Try this: ") ++ suggestionText
+    let info := Info.ofCustomInfo {
+      stx := ref
+      value := Dynamic.mk {
+        edit
+        suggestion := suggestion.toTryThisSuggestion
+        codeActionTitle
+        : TryThisInfo
+      }
+    }
     pushInfoLeaf info
-    -- The following access is safe because
-    -- `suggestionsArr = #[suggestion.toTryThisSuggestion].map ...` (see `processSuggestions`)
-    let suggestionText := suggestionArr[0]!
     let map ← getFileMap
     let rangeContents := map.source.extract range.start range.stop
     let edits ← do
@@ -464,7 +473,7 @@ def mkSuggestionsMessage (suggestions : Array Suggestion) (ref : Syntax)
           id := ``textInsertionWidget
           javascriptHash := textInsertionWidget.javascriptHash
           props := return json% {
-            range: $lspRange,
+            range: $edit.range,
             suggestion: $suggestionText,
             acceptSuggestionProps: {
               kind: "text",
@@ -479,7 +488,7 @@ def mkSuggestionsMessage (suggestions : Array Suggestion) (ref : Syntax)
         let json := json% {
           diff: $diffJson,
           suggestion: $suggestionText,
-          range: $lspRange
+          range: $edit.range
         }
         let diffString :=
           if suggestion.diffGranularity matches .none then

src/Lean/Meta/Tactic/TryThis.lean

@@ -46,24 +46,17 @@ apply the replacement.
   let doc ← readDoc
   pure <| snap.infoTree.foldInfo (init := #[]) fun _ctx info result => Id.run do
     let .ofCustomInfo { stx, value } := info | result
-    let some { range, suggestionTexts, codeActionPrefix? } :=
+    let some { edit, codeActionTitle, .. } :=
       value.get? TryThisInfo | result
     let some stxRange := stx.getRange? | result
     let stxRange := doc.meta.text.utf8RangeToLspRange stxRange
     unless stxRange.start.line ≤ params.range.end.line do return result
     unless params.range.start.line ≤ stxRange.end.line do return result
-    let mut result := result
-    for h : i in *...suggestionTexts.size do
-      let (newText, title?) := suggestionTexts[i]
-      let title := title?.getD <| (codeActionPrefix?.getD "Try this: ") ++ newText
-      result := result.push {
-        eager.title := title
-        eager.kind? := "quickfix"
-        -- Only make the first option preferred
-        eager.isPreferred? := if i = 0 then true else none
-        eager.edit? := some <| .ofTextEdit doc.versionedIdentifier { range, newText }
-      }
-    result
+    result.push {
+      eager.title := codeActionTitle
+      eager.kind? := "quickfix"
+      eager.edit? := some <| .ofTextEdit doc.versionedIdentifier edit
+    }
 
 /-! # Formatting -/
 

src/Lean/Meta/TryThis.lean

@@ -28,21 +28,6 @@ open PrettyPrinter
 
 /-! # Code action information -/
 
-/-- A packet of information about a "Try this" suggestion
-that we store in the infotree for the associated code action to retrieve. -/
-structure TryThisInfo : Type where
-  /-- The textual range to be replaced by one of the suggestions. -/
-  range : Lsp.Range
-  /--
-  A list of suggestions for the user to choose from.
-  Each suggestion may optionally come with an override for the code action title.
-  -/
-  suggestionTexts : Array (String × Option String)
-  /-- The prefix to display before the code action for a "Try this" suggestion if no custom code
-  action title is provided. If not provided, `"Try this: "` is used. -/
-  codeActionPrefix? : Option String
-  deriving TypeName
-
 /-! # `Suggestion` data -/
 
 -- TODO: we could also support `Syntax` and `Format`
@@ -180,6 +165,23 @@ instance : ToMessageData Suggestion where
 instance : Coe SuggestionText Suggestion where
   coe t := { suggestion := t }
 
+/--
+A packet of information about a "Try this" suggestion
+that we store in the infotree for the associated code action to retrieve.
+-/
+structure TryThisInfo : Type where
+  /-- Suggestion edit as it will be applied to the editor document. -/
+  edit : Lsp.TextEdit
+  /-- Title of the code action that is displayed in the code action selection dialog. -/
+  codeActionTitle : String
+  /--
+  Original suggestion that this `TryThisInfo` was derived from.
+  Stored so that meta-code downstream can extract the suggestions
+  produced by a tactic from the `InfoTree`.
+  -/
+  suggestion : Suggestion
+  deriving TypeName
+
 /-! # Formatting -/
 
 /-- Yields `(indent, column)` given a `FileMap` and a `String.Range`, where `indent` is the number
@@ -226,50 +228,16 @@ def prettyExtra (s : SuggestionText) (w : Option Nat := none)
 
 end SuggestionText
 
-/-- Converts a `Suggestion` to `Json` in `CoreM`. We need `CoreM` in order to pretty-print syntax.
-
-This also returns a `String × Option String` consisting of the pretty-printed text and any custom
-code action title if `toCodeActionTitle?` is provided.
-
-If `w := none`, then `w := getInputWidth (← getOptions)` is used.
--/
-def Suggestion.process (s : Suggestion) (w : Option Nat := none) (indent column : Nat := 0) :
-    CoreM (String × Option String) := do
-  let text ← s.suggestion.prettyExtra w indent column
-  return (text, s.toCodeActionTitle?.map (· text))
-
-/--
-Represents processed data for a collection of suggestions that can be passed to a widget and pushed
-in an info leaf.
-
-It contains the following data:
-* `suggestions`: tuples of the form `(j, t, p)` where `j` is JSON containing a suggestion and its
-  pre- and post-info, `t` is the text to be inserted by the suggestion, and `p` is the code action
-  prefix thereof.
-* `info`: the `TryThisInfo` data corresponding to a collection of suggestions
-* `range`: the range at which the suggestion is to be applied.
--/
-structure ProcessedSuggestions where
-  suggestions : Array String
-  info : Elab.Info
-  range : Lsp.Range
+def Suggestion.pretty (s : Suggestion) (w : Option Nat := none) (indent column : Nat := 0) :
+    CoreM String := do
+  s.suggestion.prettyExtra w indent column
 
-/--
-Processes an array of `Suggestion`s into data that can be used to construct a code-action info leaf
-and "try this" widget.
--/
-def processSuggestions (ref : Syntax) (range : String.Range) (suggestions : Array Suggestion)
-    (codeActionPrefix? : Option String) : CoreM ProcessedSuggestions := do
+def Suggestion.processEdit (s : Suggestion) (range : String.Range) : CoreM Lsp.TextEdit := do
   let map ← getFileMap
   -- FIXME: this produces incorrect results when `by` is at the beginning of the line, i.e.
   -- replacing `tac` in `by tac`, because the next line will only be 2 space indented
   -- (less than `tac` which starts at column 3)
   let (indent, column) := getIndentAndColumn map range
-  let suggestions ← suggestions.mapM (·.process (indent := indent) (column := column))
-  let ref := Syntax.ofRange <| ref.getRange?.getD range
+  let newText ← s.pretty (indent := indent) (column := column)
   let range := map.utf8RangeToLspRange range
-  let info := .ofCustomInfo {
-    stx := ref
-    value := Dynamic.mk { range, suggestionTexts := suggestions, codeActionPrefix? : TryThisInfo }
-  }
-  return { info, suggestions := suggestions.map (·.1), range }
+  return { range, newText }

tests/lean/interactive/builtinCodeactions.lean.expected.out

@@ -5,7 +5,6 @@
 [{"title":
   "Try this: simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n    aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h",
   "kind": "quickfix",
-  "isPreferred": true,
   "edit":
   {"documentChanges":
    [{"textDocument": {"version": 1, "uri": "file:///builtinCodeactions.lean"},