feat: adaptations for leanprover/lean4#2964

Std/Tactic/TryThis.lean

@@ -21,7 +21,7 @@ namespace Std.Tactic.TryThis
 
 open Lean Elab PrettyPrinter Meta Server RequestM
 
-/-! # Raw widgets and code actions -/
+/-! # Raw widget -/
 
 /--
 This is a widget which is placed by `TryThis.addSuggestion` and `TryThis.addSuggestions`.
@@ -40,8 +40,7 @@ Try these:
 
 where `<replacement*>` is a link which will perform the replacement.
 -/
-@[widget] def tryThisWidget : Widget.UserWidgetDefinition where
-  name := "Suggestion"
+@[widget_module] def tryThisWidget : Widget.Module where
   javascript := "
 import * as React from 'react';
 import { EditorContext } from '@leanprover/infoview';
@@ -68,42 +67,58 @@ export default function ({ pos, suggestions, range, header, isInline, style }) {
   }
 
   // Choose between an inline 'Try this'-like display and a list-based 'Try these'-like display.
+  let inner = null
   if (isInline) {
-    return e('div', { className: 'ml1' },
+    inner = e('div', { className: 'ml1' },
       e('pre', { className: 'font-code pre-wrap' }, header, makeSuggestion(suggestions[0])))
   } else {
-    return e('div', { className: 'ml1' },
+    inner = e('div', { className: 'ml1' },
       e('pre', { className: 'font-code pre-wrap' }, header),
       e('ul', { style: { paddingInlineStart: '20px' } }, suggestions.map(s =>
         e('li', { className: 'font-code pre-wrap' }, makeSuggestion(s)))))
   }
+  return e('details', { open: true },
+    e('summary', { className: 'mv2 pointer' }, 'Suggestions'),
+    inner)
 }"
 
+/-! # Code action -/
+
+/-- 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
+
 /--
 This is a code action provider that looks for `TryThisInfo` nodes and supplies a code action to
 apply the replacement.
 -/
 @[code_action_provider] def tryThisProvider : CodeActionProvider := fun params snap => do
   let doc ← readDoc
   pure <| snap.infoTree.foldInfo (init := #[]) fun _ctx info result => Id.run do
-    let .ofUserWidgetInfo { stx, widgetId := ``tryThisWidget, props } := info | result
+    let .ofCustomInfo { stx, value } := info | result
+    let some { range, suggestionTexts, codeActionPrefix? } :=
+      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 .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"
-    let codeActionPrefix :=
-      (props.getObjValAs? String "codeActionPrefix").toOption.getD "Try this: "
     let mut result := result
-    for h : i in [:suggestions.size] do
-      let suggestion := suggestions[i]'h.2
-      let .ok newText := suggestion.getObjValAs? String "suggestion" | panic! "bad type"
-      let codeActionTitle := (suggestion.getObjValAs? String "codeActionTitle").toOption.getD <|
-        codeActionPrefix ++ newText
+    for h : i in [:suggestionTexts.size] do
+      let (newText, title?) := suggestionTexts[i]'h.2
+      let title := title?.getD <| (codeActionPrefix?.getD "Try this: ") ++ newText
       result := result.push {
-        eager.title := codeActionTitle
+        eager.title := title
         eager.kind? := "quickfix"
         -- Only make the first option preferred
         eager.isPreferred? := if i = 0 then true else none
@@ -282,28 +297,25 @@ structure Suggestion where
   messageData? : Option MessageData := none
   /-- How to construct the text that appears in the lightbulb menu from the suggestion text. If
   `none`, we use `fun ppSuggestionText => "Try this: " ++ ppSuggestionText`. Only the pretty-printed
-  `suggestion : SuggestionText` is used here.
-
-  Note that (if not `none`) a prop `codeActionTitle : String` will be included in the Json, not
-  `toCodeActionTitle?` itself, as the application of `toCodeAction` to the pretty-printed
-  `suggestion : SuggestionText` must be performed before encoding. -/
+  `suggestion : SuggestionText` is used here. -/
   toCodeActionTitle? : Option (String → String) := none
   deriving Inhabited
 
 /-- 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.toJsonM (s : Suggestion) (w : Option Nat := none) (indent column : Nat := 0) :
-    CoreM Json := do
+def Suggestion.toJsonAndInfoM (s : Suggestion) (w : Option Nat := none) (indent column : Nat := 0) :
+    CoreM (Json × 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
   if let some style := s.style? then json := ("style", toJson style) :: json
-  if let some tocodeActionTitle := s.toCodeActionTitle? then
-    json := ("codeActionTitle", tocodeActionTitle text) :: json
-  return Json.mkObj json
+  return (Json.mkObj json, text, s.toCodeActionTitle?.map (· text))
 
 /- If `messageData?` is specified, we use that; otherwise (by default), we use `toMessageData` of
 the suggestion text. -/
@@ -323,28 +335,32 @@ def delabToRefinableSuggestion (e : Expr) : MetaM Suggestion :=
 element or a list display is controlled by `isInline`. -/
 private def addSuggestionCore (ref : Syntax) (suggestions : Array Suggestion)
     (header : String) (isInline : Bool) (origSpan? : Option Syntax := none)
-    (style? : Option SuggestionStyle := none) (codeActionPrefix? : Option String := none) :
-    CoreM Unit := do
+    (style? : Option SuggestionStyle := none)
+    (codeActionPrefix? : Option String := none) : CoreM Unit := do
   if let some range := (origSpan?.getD ref).getRange? then
     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 (·.toJsonM (indent := indent) (column := column))
-    let stxRange := ref.getRange?.getD range
-    let stxRange :=
-      { start := map.lineStart (map.toPosition stxRange.start).line
-        stop := map.lineStart ((map.toPosition stxRange.stop).line + 1) }
-    Widget.saveWidgetInfo ``tryThisWidget (.ofRange stxRange) (props := json% {
-      suggestions: $suggestions,
-      range: $(map.utf8RangeToLspRange range),
-      header: $header,
-      isInline: $isInline,
-      style: $style?,
-      codeActionPrefix: $codeActionPrefix?
-    })
-
+    let suggestions ← suggestions.mapM (·.toJsonAndInfoM (indent := indent) (column := column))
+    let suggestionTexts := suggestions.map (·.2)
+    let suggestions := suggestions.map (·.1)
+    let ref := Syntax.ofRange <| ref.getRange?.getD range
+    let range := map.utf8RangeToLspRange range
+    pushInfoLeaf <| .ofCustomInfo {
+      stx := ref
+      value := Dynamic.mk
+        { range, suggestionTexts, codeActionPrefix? : TryThisInfo }
+    }
+    Widget.savePanelWidgetInfo (hash tryThisWidget.javascript) ref
+      (props := return json% {
+        suggestions: $suggestions,
+        range: $range,
+        header: $header,
+        isInline: $isInline,
+        style: $style?
+      })
 
 /-- Add a "try this" suggestion. This has three effects:
 
@@ -372,11 +388,14 @@ The parameters are:
 * `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
   If not provided it defaults to `ref`.
 * `header`: a string that begins the display. By default, it is `"Try this: "`.
+* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
+  suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
 -/
 def addSuggestion (ref : Syntax) (s : Suggestion) (origSpan? : Option Syntax := none)
-    (header : String := "Try this: ") : MetaM Unit := do
+    (header : String := "Try this: ") (codeActionPrefix? : Option String := none) : MetaM Unit := do
   logInfoAt ref m!"{header}{s}"
   addSuggestionCore ref #[s] header (isInline := true) origSpan?
+    (codeActionPrefix? := codeActionPrefix?)
 
 /-- Add a list of "try this" suggestions as a single "try these" suggestion. This has three effects:
 
@@ -400,20 +419,19 @@ The parameters are:
     `suggestion` instead.
   * `toCodeActionTitle?`: an optional function `String → String` describing how to transform the
     pretty-printed suggestion text into the code action text which appears in the lightbulb menu.
-    If `none`, we simply prepend `codeActionPrefix?` to the suggestion text if provided (see
-    below), or else prepend `"Try this: "`.
+    If `none`, we simply prepend `"Try This: "` to the suggestion text.
 * `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
   If not provided it defaults to `ref`.
 * `header`: a string that precedes the list. By default, it is `"Try these:"`.
 * `style?`: a default style for all suggestions which do not have a custom `style?` set.
-* `codeActionPrefix?`: a default prefix string for code action messages in the lightbulb menu. This
-  is used for all suggestions which do not have a custom `toCodeActionTitle?`. (When `none`, the
-  default prefix is `"Try this: "`.)
+* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
+  suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
+  used.
 -/
 def addSuggestions (ref : Syntax) (suggestions : Array Suggestion)
     (origSpan? : Option Syntax := none) (header : String := "Try these:")
-    (style? : Option SuggestionStyle := none) (codeActionPrefix? : Option String := none) :
-    MetaM Unit := do
+    (style? : Option SuggestionStyle := none)
+    (codeActionPrefix? : Option String := none) : MetaM Unit := do
   if suggestions.isEmpty then throwErrorAt ref "no suggestions available"
   let msgs := suggestions.map toMessageData
   let msgs := msgs.foldl (init := MessageData.nil) (fun msg m => msg ++ m!"\n• " ++ m)
@@ -443,11 +461,14 @@ The parameters are:
   If not provided it defaults to `ref`.
 * `addSubgoalsMsg`: if true (default false), any remaining subgoals will be shown after
   `Remaining subgoals:`
+* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
+  suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
 -/
 def addExactSuggestion (ref : Syntax) (e : Expr)
-    (origSpan? : Option Syntax := none) (addSubgoalsMsg := false) : MetaM Unit := do
+    (origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
+    (codeActionPrefix? : Option String := none): MetaM Unit := do
   addSuggestion ref (← addExactSuggestionCore addSubgoalsMsg e)
-    (origSpan? := origSpan?)
+    (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
 
 /-- Add `exact e` or `refine e` suggestions.
 
@@ -458,11 +479,15 @@ The parameters are:
   If not provided it defaults to `ref`.
 * `addSubgoalsMsg`: if true (default false), any remaining subgoals will be shown after
   `Remaining subgoals:`
+* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
+  suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
+  used.
 -/
 def addExactSuggestions (ref : Syntax) (es : Array Expr)
-    (origSpan? : Option Syntax := none) (addSubgoalsMsg := false) : MetaM Unit := do
+    (origSpan? : Option Syntax := none) (addSubgoalsMsg := false)
+    (codeActionPrefix? : Option String := none) : MetaM Unit := do
   let suggestions ← es.mapM <| addExactSuggestionCore addSubgoalsMsg
-  addSuggestions ref suggestions (origSpan? := origSpan?)
+  addSuggestions ref suggestions (origSpan? := origSpan?) (codeActionPrefix? := codeActionPrefix?)
 
 /-- Add a term suggestion.
 
@@ -472,10 +497,14 @@ The parameters are:
 * `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
   If not provided it defaults to `ref`.
 * `header`: a string which precedes the suggestion. By default, it's `"Try this: "`.
+* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
+  suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
 -/
 def addTermSuggestion (ref : Syntax) (e : Expr)
-    (origSpan? : Option Syntax := none) (header : String := "Try this: ") : MetaM Unit := do
+    (origSpan? : Option Syntax := none) (header : String := "Try this: ")
+    (codeActionPrefix? : Option String := none) : MetaM Unit := do
   addSuggestion ref (← delabToRefinableSuggestion e) (origSpan? := origSpan?) (header := header)
+    (codeActionPrefix? := codeActionPrefix?)
 
 /-- Add term suggestions.
 
@@ -485,8 +514,12 @@ The parameters are:
 * `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
   If not provided it defaults to `ref`.
 * `header`: a string which precedes the list of suggestions. By default, it's `"Try these:"`.
+* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text for all
+  suggestions which do not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is
+  used.
 -/
 def addTermSuggestions (ref : Syntax) (es : Array Expr)
-    (origSpan? : Option Syntax := none) (header : String := "Try these:") : MetaM Unit := do
+    (origSpan? : Option Syntax := none) (header : String := "Try these:")
+    (codeActionPrefix? : Option String := none) : MetaM Unit := do
   addSuggestions ref (← es.mapM delabToRefinableSuggestion)
-    (origSpan? := origSpan?) (header := header)
+    (origSpan? := origSpan?) (header := header) (codeActionPrefix? := codeActionPrefix?)

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-12-19
+leanprover/lean4:nightly-2023-12-21