src/Pure/General/json.scala

--- a/src/Pure/General/json.scala	Wed Mar 09 12:41:40 2022 +0100
+++ b/src/Pure/General/json.scala	Wed Mar 09 16:21:14 2022 +0100
@@ -172,6 +172,8 @@
       try { Some(parse(s, strict = false)) }
       catch { case ERROR(_) => None }
 
+    def apply_lines(json: List[T]): S = json.map(apply).mkString("[", ",\n", "]")
+
     def apply(json: T): S =
     {
       val result = new StringBuilder