From 94a9295554c61c90c71f8564cc548801ff5805d1 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Wed, 19 Oct 2022 09:40:30 +0200
Subject: [PATCH] json without line breaks

---
 server/leanserver/GameServer/Server.lean | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/server/leanserver/GameServer/Server.lean b/server/leanserver/GameServer/Server.lean
index 46ded93..f6610a2 100644
--- a/server/leanserver/GameServer/Server.lean
+++ b/server/leanserver/GameServer/Server.lean
@@ -11,9 +11,18 @@ import GameServer.EnvExtensions
 
 open Lean Meta Elab Tactic Std
 
-/- Convert JSON to string without line breaks -/
--- TODO: this is too slow...
-instance instToStringJsonOneLine : ToString Json := ToString.mk (fun o => (toString o).replace "\n" "")
+/-- Convert format to string without line breaks -/
+def Std.Format.oneline : Format → String
+| .nil => ""
+| .line => ""
+| .text s => s
+| .nest _ f => f.oneline
+| .append f g => f.oneline ++ g.oneline
+| .group f _ => f.oneline
+| .tag _ f => f.oneline
+
+/-- Convert JSON to string without line breaks -/
+instance instToStringJsonOneLine : ToString Json := ⟨fun o => o.render.oneline⟩
 attribute [-instance] Lean.Json.instToStringJson
 
 /-! ## GameGoal -/