From 2dff3d072f6f402930576c658b5dc981db8e290e Mon Sep 17 00:00:00 2001
From: FrederickPu <119814259+FrederickPu@users.noreply.github.com>
Date: Wed, 4 Feb 2026 20:46:19 +0000
Subject: [PATCH] compress Json output to be on single line

---
 REPL/Main.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/REPL/Main.lean b/REPL/Main.lean
index 9b36b27d..bfc8ea8e 100644
--- a/REPL/Main.lean
+++ b/REPL/Main.lean
@@ -426,7 +426,7 @@ where loop : M IO Unit := do
   if query = "" then
     return ()
   if query.startsWith "#" || query.startsWith "--" then loop else
-  IO.println <| toString <| ← match ← parse query with
+  IO.println <| compress <| ← match ← parse query with
   | .command r => return toJson (← runCommand r)
   | .file r => return toJson (← processFile r)
   | .proofStep r => return toJson (← runProofStep r)