src/Tools/Graphview/graphview.scala
changeset 67547 aefe7a7b330a
parent 61590 94ab348eaab2
child 71601 97ccf48c2f0c
--- a/src/Tools/Graphview/graphview.scala	Tue Jan 30 22:46:00 2018 +0100
+++ b/src/Tools/Graphview/graphview.scala	Tue Jan 30 23:01:38 2018 +0100
@@ -75,8 +75,9 @@
     def node_text(node: Graph_Display.Node, content: XML.Body): String =
       if (show_content) {
         val s =
-          XML.content(Pretty.formatted(
-            content, options.int("graphview_content_margin").toDouble, metrics.Pretty_Metric))
+          XML.content(Pretty.formatted(content,
+            margin = options.int("graphview_content_margin").toDouble,
+            metric = metrics.Pretty_Metric))
         if (s.nonEmpty) s else node.toString
       }
       else node.toString