feat: "try this" messages with support for interactivity

src/Lean/Meta/Hint.lean

@@ -22,6 +22,103 @@ namespace Lean.Meta.Hint
 
 open Elab Tactic PrettyPrinter TryThis
 
+/--
+A widget for a clickable link (or icon) that inserts text into the document at a given position.
+
+The props to this widget are of the following form:
+```json
+{
+  "range": {
+    "start": {"line": 100, "character": 0},
+    "end":   {"line": 100, "character": 5}
+  },
+  "suggestion": "hi",
+  "acceptSuggestionProps": {
+    "kind": "text",
+    "hoverText": "Displayed on hover",
+    "linkText": "Displayed as the text of the link"
+  }
+}
+```
+... or the following form, where `codiconName` is one of the icons at
+https://microsoft.github.io/vscode-codicons/dist/codicon.html and `gaps` determines
+whether there are clickable spaces surrounding the icon:
+```json
+{
+  "range": {
+    "start": {"line": 100, "character": 0},
+    "end":   {"line": 100, "character": 5}
+  },
+  "suggestion": "hi",
+  "acceptSuggestionProps": {
+    "kind": "icon",
+    "hoverText": "Displayed on hover",
+    "codiconName": "search",
+    "gaps": true
+  }
+}
+```
+
+Note: we cannot add the `builtin_widget_module` attribute here because that would require importing
+`Lean.Widget.UserWidget`, which in turn imports much of `Lean.Elab` -- the module where we want to
+be able to use this widget. Instead, we register the attribute post-hoc when we declare the regular
+"Try This" widget in `Lean.Meta.Tactic.TryThis`.
+-/
+def textInsertionWidget : Widget.Module where
+  javascript := "
+import * as React from 'react';
+import { EditorContext, EnvPosContext } from '@leanprover/infoview';
+
+const e = React.createElement;
+export default function ({ range, suggestion, acceptSuggestionProps }) {
+  const pos = React.useContext(EnvPosContext)
+  const editorConnection = React.useContext(EditorContext)
+  function onClick() {
+    editorConnection.api.applyEdit({
+      changes: { [pos.uri]: [{ range, newText: suggestion }] }
+    })
+  }
+
+  if (acceptSuggestionProps.kind === 'text') {
+    return e('span', {
+        onClick,
+        title: acceptSuggestionProps.hoverText,
+        className: 'link pointer dim font-code',
+        style: { color: 'var(--vscode-textLink-foreground)' }
+      },
+      acceptSuggestionProps.linkText)
+  } else if (acceptSuggestionProps.kind === 'icon') {
+    if (acceptSuggestionProps.gaps) {
+      const icon = e('span', {
+        className: `codicon codicon-${acceptSuggestionProps.codiconName}`,
+        style: {
+          verticalAlign: 'sub',
+          fontSize: 'var(--vscode-editor-font-size)'
+        }
+      })
+      return e('span', {
+        onClick,
+        title: acceptSuggestionProps.hoverText,
+        className: `link pointer dim font-code`,
+        style: { color: 'var(--vscode-textLink-foreground)' }
+      }, ' ', icon, ' ')
+    } else {
+      return e('span', {
+        onClick,
+        title: acceptSuggestionProps.hoverText,
+        className: `link pointer dim font-code codicon codicon-${acceptSuggestionProps.codiconName}`,
+        style: {
+          color: 'var(--vscode-textLink-foreground)',
+          verticalAlign: 'sub',
+          fontSize: 'var(--vscode-editor-font-size)'
+        }
+      })
+    }
+
+  }
+  throw new Error('Unexpected `acceptSuggestionProps` kind: ' + acceptSuggestionProps.kind)
+}"
+
 /--
 A widget for rendering code action suggestions in error messages. Generally, this widget should not
 be used directly; instead, use `MessageData.hint`. Note that this widget is intended only for use
@@ -333,52 +430,82 @@ def mkSuggestionsMessage (suggestions : Array Suggestion) (ref : Syntax)
     (codeActionPrefix? : Option String) (forceList : Bool) : CoreM MessageData := do
   let mut msg := m!""
   for suggestion in suggestions do
-    if let some range := (suggestion.span?.getD ref).getRange? then
-      let { info, suggestions := suggestionArr, range := lspRange } ←
-        processSuggestions ref range #[suggestion.toTryThisSuggestion] codeActionPrefix?
-      pushInfoLeaf info
-      -- The following access is safe because
-      -- `suggestionsArr = #[suggestion.toTryThisSuggestion].map ...` (see `processSuggestions`)
-      let suggestionText := suggestionArr[0]!.2.1
-      let map ← getFileMap
-      let rangeContents := map.source.extract range.start range.stop
-      let edits ← do
-        if let some msgData := suggestion.messageData? then
-          pure #[(.insert, toString <| ← msgData.format)]
-        else
-          pure <| readableDiff rangeContents suggestionText suggestion.diffGranularity
-      let mut edits := edits
-      if let some previewRange := suggestion.previewSpan? >>= Syntax.getRange? then
-        if previewRange.includes range then
-          let map ← getFileMap
-          if previewRange.start < range.start then
-            edits := #[(.skip, (map.source.extract previewRange.start range.start))] ++ edits
-          if range.stop < previewRange.stop then
-            edits := edits.push (.skip, (map.source.extract range.stop previewRange.stop))
-      let diffJson := mkDiffJson edits
-      let json := json% {
-        diff: $diffJson,
-        suggestion: $suggestionText,
-        range: $lspRange
+    let some range := suggestion.span?.getD ref |>.getRange?
+      | continue
+    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
       }
-      let preInfo := suggestion.preInfo?.getD ""
-      let postInfo := suggestion.postInfo?.getD ""
-      let diffString :=
-        if suggestion.diffGranularity matches .none then
-          edits.foldl (· ++ ·.2) ""
-        else
-          mkDiffString edits
-      let widget := MessageData.ofWidget {
-          id := ``tryThisDiffWidget
-          javascriptHash := tryThisDiffWidget.javascriptHash
-          props := return json
-        } diffString
-      let widgetMsg := m!"{preInfo}{widget}{postInfo}"
-      let suggestionMsg := if suggestions.size == 1 && !forceList then
-        m!"\n{widgetMsg}"
+    }
+    pushInfoLeaf info
+    let map ← getFileMap
+    let rangeContents := map.source.extract range.start range.stop
+    let edits ← do
+      if let some msgData := suggestion.messageData? then
+        pure #[(.insert, toString <| ← msgData.format)]
       else
-        m!"\n" ++ MessageData.nest 2 m!"• {widgetMsg}"
-      msg := msg ++ MessageData.nestD suggestionMsg
+        pure <| readableDiff rangeContents suggestionText suggestion.diffGranularity
+    let mut edits := edits
+    if let some previewRange := suggestion.previewSpan? >>= Syntax.getRange? then
+      if previewRange.includes range then
+        let map ← getFileMap
+        if previewRange.start < range.start then
+          edits := #[(.skip, (map.source.extract previewRange.start range.start))] ++ edits
+        if range.stop < previewRange.stop then
+          edits := edits.push (.skip, (map.source.extract range.stop previewRange.stop))
+    let preInfo := suggestion.preInfo?.getD ""
+    let postInfo := suggestion.postInfo?.getD ""
+    let isDiffSuggestion :=
+      ! (suggestion.diffGranularity matches .none) && suggestion.messageData?.isNone
+        || suggestion.previewSpan?.isSome
+    let suggestionMsg :=
+      if ! isDiffSuggestion then
+        let applyButton := MessageData.ofWidget {
+          id := ``textInsertionWidget
+          javascriptHash := textInsertionWidget.javascriptHash
+          props := return json% {
+            range: $edit.range,
+            suggestion: $suggestionText,
+            acceptSuggestionProps: {
+              kind: "text",
+              hoverText: "Apply suggestion",
+              linkText: "[apply]"
+            }
+          }
+        } "[apply]"
+        m!"\n{applyButton} {preInfo}{toMessageData suggestion}{postInfo}"
+      else
+        let diffJson := mkDiffJson edits
+        let json := json% {
+          diff: $diffJson,
+          suggestion: $suggestionText,
+          range: $edit.range
+        }
+        let diffString :=
+          if suggestion.diffGranularity matches .none then
+            edits.foldl (· ++ ·.2) ""
+          else
+            mkDiffString edits
+        let diffWidget := MessageData.ofWidget {
+            id := ``tryThisDiffWidget
+            javascriptHash := tryThisDiffWidget.javascriptHash
+            props := return json
+          } diffString
+        let msg := m!"{preInfo}{diffWidget}{postInfo}"
+        if suggestions.size == 1 && !forceList then
+          m!"\n{msg}"
+        else
+          m!"\n" ++ MessageData.nest 2 m!"• {msg}"
+    msg := msg ++ MessageData.nestD suggestionMsg
   return msg
 
 /--

src/Lean/Meta/Tactic/TryThis.lean

@@ -34,6 +34,7 @@ open Lean Elab Tactic PrettyPrinter Meta Server RequestM
 
 -- Because we can't use `builtin_widget_module` in `Lean.Meta.Hint`, we add the attribute here
 attribute [builtin_widget_module] Hint.tryThisDiffWidget
+attribute [builtin_widget_module] Hint.textInsertionWidget
 
 /-! # Code action -/
 
@@ -45,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 -/
 
@@ -72,7 +66,7 @@ def delabToRefinableSyntax (e : Expr) : MetaM Term :=
 
 /-- Delaborate `e` into a suggestion suitable for use by `refine`. -/
 def delabToRefinableSuggestion (e : Expr) : MetaM Suggestion :=
-  return { suggestion := ← delabToRefinableSyntax e }
+  return { suggestion := ← delabToRefinableSyntax e, messageData? := ← addMessageContext <| toMessageData e }
 
 /-- Add a "try this" suggestion. This has two effects:
 
@@ -187,19 +181,19 @@ Remark: We cannot determine if a tactic requires `expose_names` merely by inspec
 (shadowed variables are delaborated without daggers) nor the underlying `Expr` used to produce it
 (some inaccessible names may be implicit arguments that do not appear in the delaborated syntax).
 -/
-private def mkValidatedTactic (tac : TSyntax `tactic)
+private def mkValidatedTactic (tac : TSyntax `tactic) (msg : MessageData)
     (initialState : Tactic.SavedState) (expectedType? : Option Expr := none) :
-    TacticM (Option (TSyntax `tactic)) := do
+    TacticM (Option (TSyntax `tactic × MessageData)) := do
   try
     evalTacticWithState initialState tac expectedType?
-    return some tac
+    return some (tac, msg)
   catch _ =>
     -- Note: we must use `(expose_names; _)` and not `· expose_names; _` to avoid generating
     -- spurious tactic-abort exceptions, since these tactics may not close the goal
     let tac ← `(tactic| (expose_names; $tac))
     try
       evalTacticWithState initialState tac expectedType?
-      return some tac
+      return some (tac, m!"(expose_names; {msg})")
     catch _ =>
       return none
 
@@ -231,7 +225,7 @@ private def addExactSuggestionCore (addSubgoalsMsg : Bool) (checkState? : Option
   let hasMVars := !mvars.isEmpty
   let (suggestion, messageData) ← mkExactSuggestionSyntax e (useRefine := hasMVars)
   let some checkState := checkState? | return .inl suggestion
-  let some suggestion ← mkValidatedTactic suggestion checkState
+  let some (suggestion, messageData) ← mkValidatedTactic suggestion messageData checkState
     | let messageData := m!"(expose_names; {messageData})"
       return .inr <| mkFailedToMakeTacticMsg m!"a {if hasMVars then "partial " else ""}proof" messageData
   let postInfo? ← if !addSubgoalsMsg || mvars.isEmpty then pure none else
@@ -241,7 +235,7 @@ private def addExactSuggestionCore (addSubgoalsMsg : Bool) (checkState? : Option
       let e ← withExposedNames <| PrettyPrinter.ppExpr (← instantiateMVars (← g.getType))
       str := str ++ Format.pretty ("\n-- ⊢ " ++ e)
     pure str
-  return .inl { suggestion := suggestion, postInfo? }
+  return .inl { suggestion := suggestion, postInfo?, messageData? := messageData }
 
 /-- Add an `exact e` or `refine e` suggestion.
 
@@ -374,11 +368,12 @@ def addHaveSuggestion (ref : Syntax) (h? : Option Name) (t? : Option Expr) (e :
         pure (← `(tactic| let $(mkIdent h):ident := $estx), m!"let {h} := {e}")
     pure (tac, ← addMessageContext msg)
   if let some checkState := checkState? then
-    let some tac' ← mkValidatedTactic tac checkState
+    let some (tac', msg') ← mkValidatedTactic tac msg checkState
       | logInfo <| mkFailedToMakeTacticMsg "a proof" msg
         return
     tac := tac'
-  addSuggestion ref (s := { suggestion := tac }) origSpan?
+    msg := msg'
+  addSuggestion ref (s := { suggestion := tac, messageData? := msg }) origSpan?
 
 open Lean.Parser.Tactic
 open Lean.Syntax
@@ -400,7 +395,7 @@ def addRewriteSuggestion (ref : Syntax) (rules : List (Expr × Bool))
   (type? : LOption Expr := .undef) (loc? : Option Expr := none)
   (origSpan? : Option Syntax := none) (checkState? : Option Tactic.SavedState := none) :
     TacticM Unit := do
-  let mut (tac, tacMsg, extraMsg, extraStr) ← withExposedNames do
+  let mut (tac, tacMsg, extraMsg) ← withExposedNames do
     let rulesStx := TSepArray.ofElems <| ← rules.toArray.mapM fun ⟨e, symm⟩ => do
       let t ← delabToRefinableSyntax e
       if symm then `(rwRule| ← $t:term) else `(rwRule| $t:term)
@@ -423,22 +418,23 @@ def addRewriteSuggestion (ref : Syntax) (rules : List (Expr × Bool))
       else
         m!"rw {rulesMsg}"
 
-    let (extraMsg, extraStr) ←
+    let extraMsg ←
       match type? with
       | .some type =>
-        pure (← addMessageContext m!"\n-- {type}", s!"\n-- {← PrettyPrinter.ppExpr type}")
-      | .none => pure (m!"\n-- no goals", "\n-- no goals")
-      | .undef => pure (m!"", "")
-    return (tac, tacMsg, extraMsg, extraStr)
+        pure <| ← addMessageContext m!"\n-- {type}"
+      | .none => pure m!"\n-- no goals"
+      | .undef => pure m!""
+    return (tac, tacMsg, extraMsg)
 
   if let some checkState := checkState? then
     let type? := match type? with
       | .some type => some type
       | _ => none
-    let some tac' ← mkValidatedTactic tac checkState type?
+    let some (tac', tacMsg') ← mkValidatedTactic tac tacMsg checkState type?
       | tacMsg := m!"(expose_names; {tacMsg})"
         logInfo <| mkFailedToMakeTacticMsg "an applicable rewrite lemma" (tacMsg ++ extraMsg)
         return
     tac := tac'
-  addSuggestion ref (s := { suggestion := tac, postInfo? := extraStr })
+    tacMsg := tacMsg'
+  addSuggestion ref (s := { suggestion := tac, messageData? := tacMsg ++ extraMsg })
     origSpan?