diff --git a/src/Lean/Meta/Hint.lean b/src/Lean/Meta/Hint.lean index 1f87f1e99e..814254337c 100644 --- a/src/Lean/Meta/Hint.lean +++ b/src/Lean/Meta/Hint.lean @@ -342,7 +342,12 @@ def mkSuggestionsMessage (suggestions : Array Suggestion) (ref : Syntax) let suggestionText := suggestionArr[0]!.2.1 let map ← getFileMap let rangeContents := map.source.extract range.start range.stop - let mut edits := readableDiff rangeContents suggestionText suggestion.diffGranularity + 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 diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean index 5893d5912d..4564f1d36b 100644 --- a/src/Lean/Meta/Tactic/TryThis.lean +++ b/src/Lean/Meta/Tactic/TryThis.lean @@ -88,6 +88,8 @@ The parameters are: message (only) * `postInfo?`: an optional string shown immediately after the replacement text in the widget message (only) + * `messageData?`: an optional `MessageData` displayed instead of `suggestion`. + If set, implies `diffGranularity = .none`. * `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 `"Try This: "` to the suggestion text. @@ -125,6 +127,8 @@ The parameters are: message (only) * `postInfo?`: an optional string shown immediately after the replacement text in the widget message (only) + * `messageData?`: an optional `MessageData` displayed instead of `suggestion`. + If set, implies `diffGranularity = .none`. * `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 `"Try this: "` to the suggestion text. diff --git a/src/Lean/Meta/TryThis.lean b/src/Lean/Meta/TryThis.lean index 5e83133994..2bf93a521b 100644 --- a/src/Lean/Meta/TryThis.lean +++ b/src/Lean/Meta/TryThis.lean @@ -161,7 +161,8 @@ structure Suggestion where Note that this property is used only by the "try this" widget; it is ignored by the inline hint widget. -/ style? : Option SuggestionStyle := none - /-- How to represent the suggestion as `MessageData`. This is used only in the info diagnostic. + /-- How to represent the suggestion as `MessageData`. This is used only in the text of the + widget diagnostic. If `none`, we use `suggestion`. Use `toMessageData` to render a `Suggestion` in this manner. -/ messageData? : Option MessageData := none /-- How to construct the text that appears in the lightbulb menu from the suggestion text. If @@ -171,7 +172,6 @@ structure Suggestion where deriving Inhabited attribute [deprecated "The `style?` property is not used anymore." (since := "2025-08-14")] Suggestion.style? -attribute [deprecated "The `messageData?` property is not used anymore." (since := "2025-08-14")] Suggestion.messageData? /- Use `toMessageData` of the suggestion text. -/ instance : ToMessageData Suggestion where