max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: re-enable Suggestion.messageData? (#10157)

Browse source 
Re-enables `Suggestion.messageData?` after it was deprecated in #9966
since it is needed for the workaround described in #10150. We will
hopefully be able to clean up with API once #10150 is properly fixed.
This commit is contained in:
Marc Huisinga 2025-08-27 18:23:02 +02:00 • committed by GitHub
parent 2dda33ddb2
commit 3ce69e4edb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 12 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Meta/Hint.lean
View file

@ -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

4
src/Lean/Meta/Tactic/TryThis.lean
View file

@ -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.

4
src/Lean/Meta/TryThis.lean
View file

@ -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