--- 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 =