Partially fix Try this indentation

Aesop/Search/Main.lean

@@ -165,7 +165,7 @@ def traceScript : SearchM Q Unit := do
     let script ← script.render tacticState
     if options.traceScript then
       let script ← `(tacticSeq| $script*)
-      Std.Tactic.TryThis.addSuggestion (← getRef) script
+      addTryThisTacticSeqSuggestion (← getRef) script
     if ← Check.script.isEnabled then
       checkRenderedScript script
   catch e =>

Aesop/Util/Basic.lean

@@ -8,8 +8,10 @@ import Aesop.Nanos
 import Aesop.Util.UnionFind
 import Aesop.Util.UnorderedArraySet
 import Std.Lean.Expr
+import Std.Lean.Format
 import Std.Lean.Meta.DiscrTree
 import Std.Lean.PersistentHashSet
+import Std.Tactic.TryThis
 
 open Lean
 open Lean.Meta
@@ -310,4 +312,43 @@ where
     | .app f e => go (args.push e) f
     | _ => return (e, args.reverse)
 
+-- Largely copy-pasta from Std.Tactic.TryThis.addSuggestion
+-- I don't really know what's going on here; this is all cargo-culted. It seems
+-- to work when `aesop?` appears on its own line, as in
+--
+-- ```lean
+-- by
+--   aesop?
+-- ```
+--
+-- It doesn't work when `aesop?` is preceded by other text on the same line, as
+-- in
+--
+-- ```lean
+-- have x := by aesop?
+-- ```
+--
+-- Also, the `Try this:` suggestion in the infoview is not properly formatted.
+def addTryThisTacticSeqSuggestion (ref : Syntax)
+    (suggestion : TSyntax ``Lean.Parser.Tactic.tacticSeq)
+    (origSpan? : Option Syntax := none)
+    (extraMsg : String := "") : MetaM Unit := do
+  let fmt ← PrettyPrinter.ppCategory ``Lean.Parser.Tactic.tacticSeq suggestion
+  let text := fmt.prettyExtra (indent := 0) (column := 0)
+  logInfoAt ref m!"Try this:\n  {text}"
+  if let some range := (origSpan?.getD ref).getRange? then
+    let map ← getFileMap
+    let start := findLineStart map.source range.start
+    let indent := (range.start - start).1
+    let text := fmt.prettyExtra (indent := indent - 2) (column := indent)
+    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) }
+    let range := map.utf8RangeToLspRange range
+    let json := Json.mkObj
+      [("suggestion", text), ("range", toJson range), ("info", extraMsg)]
+    Widget.saveWidgetInfo ``Std.Tactic.TryThis.tryThisWidget json
+      (.ofRange stxRange)
+
 end Aesop

tests/ScriptWithOptions.lean.expected

@@ -1 +1,2 @@
-Try this: simp_all only
+Try this:
+  simp_all only

tests/TryThisIndentation.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2023 Jannis Limperg. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jannis Limperg
+-/
+
+import Aesop
+
+set_option trace.debug true
+
+example {a y : α} {l : List α} : a ≠ y → a ∉ l → a ∉ y::l := by
+  aesop?
+
+example {a y : α} {l : List α} : a ≠ y → a ∉ l → a ∉ y::l := by
+  intros
+  have : ¬ a ∈ y :: l := by
+    aesop?
+  exact this

tests/TryThisIndentation.lean.expected

@@ -0,0 +1,6 @@
+Try this:
+  intro a_1 a_2
+  simp_all only [ne_eq, List.mem_cons, or_self, not_false_eq_true]
+Try this:
+  rename_i a_1 a_2
+  simp_all only [ne_eq, List.mem_cons, or_self, not_false_eq_true]