Skip to content

Commit

Permalink
Fix wrapping of "Try this" suggestion
Browse files Browse the repository at this point in the history
We used to pass the wrong arguments to `fmt.pretty` when formatting the
`Try this` replacement text (but not the infoview message). As a result,
the formatter was using a line width that was much too small.
  • Loading branch information
JLimperg committed May 27, 2024
1 parent 206f29e commit 70ec1d9
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Aesop/Util/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -367,7 +367,7 @@ def addTryThisTacticSeqSuggestion (ref : Syntax)
if let some range := (origSpan?.getD ref).getRange? then
let map ← getFileMap
let (indent, column) := Lean.Meta.Tactic.TryThis.getIndentAndColumn map range
let text := fmt.pretty indent column
let text := fmt.pretty (indent := indent) (column := column)
let suggestion := {
-- HACK: The `tacticSeq` syntax category is pretty-printed with each line
-- indented by two spaces (for some reason), so we remove this
Expand Down

0 comments on commit 70ec1d9

Please sign in to comment.