tuned for scala3;
authorwenzelm
Mon, 04 Apr 2022 22:06:40 +0200
changeset 75403 0f80086c000e
parent 75402 42fe20507496
child 75404 a1363da718aa
tuned for scala3;
src/Pure/General/json_api.scala
src/Tools/Graphview/layout.scala
--- a/src/Pure/General/json_api.scala	Mon Apr 04 22:04:20 2022 +0200
+++ b/src/Pure/General/json_api.scala	Mon Apr 04 22:06:40 2022 +0200
@@ -26,7 +26,7 @@
   }
 
   sealed case class Root(json: JSON.T) {
-    def get_links: Option[Links] = JSON.value(json, "links").map(Links)
+    def get_links: Option[Links] = JSON.value(json, "links").map(Links.apply)
     def get_next: Option[Service] = get_links.flatMap(_.get_next)
 
     def get_included: List[Resource] = JSON.list(json, "included", Resource.some).getOrElse(Nil)
--- a/src/Tools/Graphview/layout.scala	Mon Apr 04 22:04:20 2022 +0200
+++ b/src/Tools/Graphview/layout.scala	Mon Apr 04 22:06:40 2022 +0200
@@ -107,7 +107,7 @@
                 val lines = split_lines(node_text(a, content))
                 val w2 = metrics.node_width2(lines)
                 val h2 = metrics.node_height2(lines.length)
-                ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node))
+                ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node.apply))
             }).toList)
 
       val initial_levels: Levels =