feat(repl): Improve tomograph's info

Pantograph/Frontend/InfoTree.lean

@@ -131,16 +131,16 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
   | .node info children =>
     if let some ctx := ctx? then
       let node : String ← match info with
-      | .ofTermInfo    info => pure s!"[term] {(← info.toString ctx)}"
+      | .ofTermInfo    info => pure s!"[term] {info.stx}"
-      | .ofCommandInfo info => pure s!"[command] {(← info.toString ctx)}"
+      | .ofCommandInfo info => pure s!"[command] {info.stx}"
-      | .ofTacticInfo  info => pure s!"[tactic] {(← info.toString ctx)}"
+      | .ofTacticInfo  info => pure s!"[tactic] {info.stx}"
       | .ofMacroExpansionInfo _ => pure "[macro_exp]"
-      | .ofOptionInfo _ => pure "[option]"
+      | .ofOptionInfo info => pure s!"[option] {info.stx}"
       | .ofFieldInfo _ => pure "[field]"
-      | .ofCompletionInfo _ => pure "[completion]"
+      | .ofCompletionInfo info => pure s!"[completion] {info.stx}"
       | .ofUserWidgetInfo _ => pure "[user_widget]"
       | .ofCustomInfo _ => pure "[custom]"
-      | .ofFVarAliasInfo _ => pure "[fvar]"
+      | .ofFVarAliasInfo _ => pure "[fvar_alias]"
       | .ofFieldRedeclInfo _ => pure "[field_redecl]"
       | .ofChoiceInfo _ => pure "[choice]"
       | .ofPartialTermInfo  _ => pure "[partial_term]"

Tomograph.lean

@@ -1,29 +1,36 @@
+/- A tool for analysing Lean source code. -/
 import Pantograph.Frontend
 
 open Lean
 
 namespace Pantograph
 
-def fail (s : String) : IO Unit := do
+def fail (s : String) : IO UInt32 := do
   IO.eprintln s
+  return 2
 
-def dissect (args: List String): IO Unit := do
+def dissect (args: List String): IO UInt32 := do
   let fileName :: _args := args | fail s!"Must supply a file name"
   let file ← IO.FS.readFile fileName
   let (context, state) ← do Frontend.createContextStateFromFile file fileName (env? := .none) {}
   let frontendM: Elab.Frontend.FrontendM _ :=
     Frontend.mapCompilationSteps λ step => do
-      for tree in step.trees do
+      IO.println s!"🐈 {step.stx.getKind.toString}"
-        IO.println s!"{← tree.toString}"
+      for (tree, i) in step.trees.zipIdx do
+        IO.println s!"🌲[{i}] {← tree.toString}"
   let (_, _) ← frontendM.run context |>.run state
-  return ()
+  return 0
 
 end Pantograph
 
 open Pantograph
 
-def main (args : List String) : IO Unit := do
+def help : IO UInt32 := do
-  let command :: args := args | IO.eprintln "Must supply a command"
+  IO.println "Usage: tomograph dissect FILE_NAME"
+  return 1
+
+def main (args : List String) : IO UInt32 := do
+  let command :: args := args | help
   match command with
   | "dissect" => dissect args
-  | _ => IO.eprintln s!"Unknown command {command}"
+  | _ => fail s!"Unknown command {command}"