From 762a139e7800bc08bc27c2f6a9aa3ba8365fcf44 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 9 Sep 2024 12:30:32 -0700 Subject: [PATCH] feat: Export frontend functions --- Pantograph/Frontend/Basic.lean | 1 + Pantograph/Frontend/Elab.lean | 1 + 2 files changed, 2 insertions(+) diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean index 79d3ea1..933424c 100644 --- a/Pantograph/Frontend/Basic.lean +++ b/Pantograph/Frontend/Basic.lean @@ -8,6 +8,7 @@ namespace Lean.FileMap /-- Extract the range of a `Syntax` expressed as lines and columns. -/ -- Extracted from the private declaration `Lean.Elab.formatStxRange`, -- in `Lean.Elab.InfoTree.Main`. +@[export pantograph_frontend_stx_range] protected def stxRange (fileMap : FileMap) (stx : Syntax) : Position × Position := let pos := stx.getPos?.getD 0 let endPos := stx.getTailPos?.getD pos diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index 8deac23..2ff9a2e 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -88,6 +88,7 @@ structure TacticInvocation where namespace TacticInvocation /-- Return the range of the tactic, as a pair of file positions. -/ +@[export pantograph_frontend_tactic_invocation_range] protected def range (t : TacticInvocation) : Position × Position := t.ctx.fileMap.stxRange t.info.stx /-- Pretty print a tactic. -/