src/Pure/General/json.scala
changeset 73340 0ffcad1f6130
parent 71776 5ef7f374e0f8
child 75252 41dfe941c3da
--- 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"