From 3ce69e4edb7f8314437a1235de22748bce6349c5 Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Wed, 27 Aug 2025 18:23:02 +0200 Subject: [PATCH] feat: re-enable `Suggestion.messageData?` (#10157) 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. --- src/Lean/Meta/Hint.lean | 7 ++++++- src/Lean/Meta/Tactic/TryThis.lean | 4 ++++ src/Lean/Meta/TryThis.lean | 4 ++-- 3 files changed, 12 insertions(+), 3 deletions(-) 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