aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 2 Packages Projects Releases Wiki Activity

feat(frontend): Improve `InfoTree` printing

This commit is contained in:
Leni Aniva 2025-07-11 20:00:05 -07:00
parent a7ce9ed2a4
commit c287d14f86
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
1 changed files with 8 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
Pantograph/Frontend/InfoTree.lean
View File

@ -10,7 +10,6 @@ namespace Lean.Elab
private def elaboratorToString : Name → String private def elaboratorToString : Name → String
| .anonymous => "" | .anonymous => ""
| n => s!"⟨{n}⟩ " | n => s!"⟨{n}⟩ "
private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map (" " ++ .)
/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/ /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
protected def Info.stx? : Info → Option Syntax protected def Info.stx? : Info → Option Syntax
@ -125,7 +124,9 @@ partial def InfoTree.findAllInfoM [Monad m]
| _ => return [] | _ => return []
@[export pantograph_infotree_to_string_m] @[export pantograph_infotree_to_string_m]
partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .none) : IO String := do partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .none) (indent : Nat := 0)
: IO String := do
let space := String.join $ List.replicate indent " "
match t with match t with
| .context ctx t => t.toString (ctx.mergeIntoOuter? ctx?) | .context ctx t => t.toString (ctx.mergeIntoOuter? ctx?)
| .node info children => | .node info children =>
@ -145,13 +146,15 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
| .ofChoiceInfo _ => pure "[choice]" | .ofChoiceInfo _ => pure "[choice]"
| .ofPartialTermInfo _ => pure "[partial_term]" | .ofPartialTermInfo _ => pure "[partial_term]"
| .ofDelabTermInfo _ => pure "[delab_term]" | .ofDelabTermInfo _ => pure "[delab_term]"
let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx) let children ← children.toList.mapM λ t' => do
return s!"{node}\n{children}" t'.toString ctx (indent := indent + 1)
let children := String.join children
return s!"{space}{node}\n{children}"
else throw <| IO.userError "No `ContextInfo` available." else throw <| IO.userError "No `ContextInfo` available."
| .hole mvarId => | .hole mvarId =>
if let some ctx := ctx? then if let some ctx := ctx? then
let payload := (← ctx.runMetaM {} (do Meta.ppGoal mvarId)).pretty let payload := (← ctx.runMetaM {} (do Meta.ppGoal mvarId)).pretty
return s!"[hole] {payload}" return s!"{space}[hole] {payload}"
else throw <| IO.userError "No `ContextInfo` available." else throw <| IO.userError "No `ContextInfo` available."
end Lean.Elab end Lean.Elab