From 48046b8b5a522e1cb7e7e234c7e2b6f127c4142d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 2 Jul 2025 15:13:43 -0700 Subject: [PATCH] fix(tomograph): Import search directory --- Tomograph.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Tomograph.lean b/Tomograph.lean index b23ec70..26db934 100644 --- a/Tomograph.lean +++ b/Tomograph.lean @@ -1,5 +1,6 @@ /- A tool for analysing Lean source code. -/ import Pantograph.Frontend +import Pantograph.Library open Lean @@ -18,6 +19,8 @@ def dissect (args: List String): IO UInt32 := do IO.println s!"🐈 {step.stx.getKind.toString}" for (tree, i) in step.trees.zipIdx do IO.println s!"🌲[{i}] {← tree.toString}" + for (msg, i) in step.msgs.zipIdx do + IO.println s!"🔈[{i}] {← msg.toString}" let (_, _) ← frontendM.run context |>.run state return 0 @@ -31,6 +34,8 @@ def help : IO UInt32 := do def main (args : List String) : IO UInt32 := do let command :: args := args | help + unsafe do + Pantograph.initSearch "" match command with | "dissect" => dissect args | _ => fail s!"Unknown command {command}"