# HG changeset patch
# User wenzelm
# Date 1649102800 -7200
# Node ID 0f80086c000e6ca2ecf11967ea79a34e18dc1c03
# Parent  42fe20507496014316751c033c57946362b620e9
tuned for scala3;

diff -r 42fe20507496 -r 0f80086c000e src/Pure/General/json_api.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)
diff -r 42fe20507496 -r 0f80086c000e src/Tools/Graphview/layout.scala
--- 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 =