diff -r 9efdebe24c65 -r 0ffcad1f6130 src/Pure/General/json.scala --- 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"