feat: "try this" messages with support for interactivity

Author: mhuisi

src/Lean/Meta/Hint.lean

@@ -22,6 +22,61 @@ namespace Lean.Meta.Hint
 
 open Elab Tactic PrettyPrinter 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 +388,73 @@ 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 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}"
+    let some range := suggestion.span?.getD ref |>.getRange?
+      | continue
+    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]!
+    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 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: $lspRange,
+            suggestion: $suggestionText,
+            acceptSuggestionProps: {
+              kind: "text",
+              hoverText: "Apply suggestion",
+              linkText: "[apply]"
+            }
+          }
+        } "[apply]"
+        m!"\n{applyButton} {preInfo}{toMessageData suggestion}{postInfo}"
       else
-        m!"\n" ++ MessageData.nest 2 m!"• {widgetMsg}"
-      msg := msg ++ MessageData.nestD suggestionMsg
+        let diffJson := mkDiffJson edits
+        let json := json% {
+          diff: $diffJson,
+          suggestion: $suggestionText,
+          range: $lspRange
+        }
+        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 -/
 
@@ -72,7 +73,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? := e }
 
 /-- Add a "try this" suggestion. This has two effects:
 
@@ -187,19 +188,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 +232,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 +242,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 +375,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 +402,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 +425,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?

src/Lean/Meta/TryThis.lean

@@ -175,7 +175,7 @@ attribute [deprecated "The `style?` property is not used anymore." (since := "20
 
 /- Use `toMessageData` of the suggestion text. -/
 instance : ToMessageData Suggestion where
-  toMessageData s := toMessageData s.suggestion
+  toMessageData s := s.messageData?.getD (toMessageData s.suggestion)
 
 instance : Coe SuggestionText Suggestion where
   coe t := { suggestion := t }
@@ -233,13 +233,10 @@ code action title if `toCodeActionTitle?` is provided.
 
 If `w := none`, then `w := getInputWidth (← getOptions)` is used.
 -/
-def Suggestion.toJsonAndInfoM (s : Suggestion) (w : Option Nat := none) (indent column : Nat := 0) :
-    CoreM (Json × String × Option String) := do
+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
-  let mut json := [("suggestion", (text : Json))]
-  if let some preInfo := s.preInfo? then json := ("preInfo", preInfo) :: json
-  if let some postInfo := s.postInfo? then json := ("postInfo", postInfo) :: json
-  return (Json.mkObj json, text, s.toCodeActionTitle?.map (· text))
+  return (text, s.toCodeActionTitle?.map (· text))
 
 /--
 Represents processed data for a collection of suggestions that can be passed to a widget and pushed
@@ -253,7 +250,7 @@ It contains the following data:
 * `range`: the range at which the suggestion is to be applied.
 -/
 structure ProcessedSuggestions where
-  suggestions : Array (Json × String × Option String)
+  suggestions : Array String
   info : Elab.Info
   range : Lsp.Range
 
@@ -268,12 +265,11 @@ def processSuggestions (ref : Syntax) (range : String.Range) (suggestions : Arra
   -- 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 (·.toJsonAndInfoM (indent := indent) (column := column))
-  let suggestionTexts := suggestions.map (·.2)
+  let suggestions ← suggestions.mapM (·.process (indent := indent) (column := column))
   let ref := Syntax.ofRange <| ref.getRange?.getD range
   let range := map.utf8RangeToLspRange range
   let info := .ofCustomInfo {
     stx := ref
-    value := Dynamic.mk { range, suggestionTexts, codeActionPrefix? : TryThisInfo }
+    value := Dynamic.mk { range, suggestionTexts := suggestions, codeActionPrefix? : TryThisInfo }
   }
-  return { info, suggestions, range }
+  return { info, suggestions := suggestions.map (·.1), range }

tests/lean/4591.lean.expected.out

@@ -1,2 +1,2 @@
 Try this:
-  simp only [Nat.foo]
+  [apply] simp only [Nat.foo]