Compare commits

..

1 Commits

Author SHA1 Message Date
Leni Aniva 9a36c6fbeb
chore: Update version to 0.3.5 2025-07-11 20:57:57 -07:00
2 changed files with 6 additions and 9 deletions

View File

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

View File

@ -1,6 +1,6 @@
namespace Pantograph
@[export pantograph_version]
def version := "0.3.4"
def version := "0.3.5"
end Pantograph