From 37a5884be40790a946e0b8e26879ed3bbf509077 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Dec 2024 21:39:33 -0800 Subject: [PATCH] fix: Use `ppSyntax` instead of `ppTactic` --- Pantograph/Frontend/Elab.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index a33fbef..d9480f0 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -87,9 +87,11 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc tactics.mapM λ invocation => do let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty - let tactic ← invocation.ctx.runMetaM {} do - let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ - return t.pretty + let tactic ← invocation.ctx.runMetaM {} <| Meta.withMCtx invocation.info.mctxBefore do + return (← invocation.ctx.ppSyntax {} invocation.info.stx).pretty + -- FIXME: Why does this not work? There are problems with `term.pseudo.antiquot` + --PrettyPrinter.ppTactic ⟨invocation.info.stx⟩ + --return t.pretty let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString return { goalBefore,