--- a/src/Pure/General/json.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/General/json.scala Mon Mar 01 22:22:12 2021 +0100
@@ -176,7 +176,7 @@
{
val result = new StringBuilder
- def string(s: String)
+ def string(s: String): Unit =
{
result += '"'
result ++=
@@ -195,7 +195,7 @@
result += '"'
}
- def array(list: List[T])
+ def array(list: List[T]): Unit =
{
result += '['
Library.separate(None, list.map(Some(_))).foreach({
@@ -205,7 +205,7 @@
result += ']'
}
- def object_(obj: Object.T)
+ def object_(obj: Object.T): Unit =
{
result += '{'
Library.separate(None, obj.toList.map(Some(_))).foreach({
@@ -218,7 +218,7 @@
result += '}'
}
- def json_format(x: T)
+ def json_format(x: T): Unit =
{
x match {
case null => result ++= "null"