Single line json formatting

Stream: Is there code for X?

[Adam Topaz]

Do we have some function (perhaps in std4?) that formats a Lean.Json as a single line?
Here's a version I hacked together, but I would prefer to use something that already exists (if it exists):

partial def Json.toLine (j : Json) : String :=
  match j with
  | .obj obj => "{" ++
      (obj.toArray.foldl (fun s ⟨key,j⟩ =>
        s ++ s!"\"{key}\":" ++ Json.toLine j ++ ",") "").dropRight 1
      ++ "}"
  | .arr arr => "[" ++
      (arr.foldl (fun s j => s ++ Json.toLine j ++ ",") "").dropRight 1
      ++ "]"
  | e => toString e

[Scott Morrison]

I'd guess not. The only JSON library we have (?) is the one in core, which is not intended for general use (i.e. does exactly what they need, and no more).

[Gabriel Ebner]

Are you missing anything from Json.compress?

[Adam Topaz]

oh, I didn't know about compress

[Adam Topaz]

Indeed, it seems like Json.compress is exactly what I was looking for! Thanks!