src/Tools/Graphview/graphview.scala

--- a/src/Tools/Graphview/graphview.scala	Mon Nov 04 14:50:21 2024 +0100
+++ b/src/Tools/Graphview/graphview.scala	Mon Nov 04 20:55:01 2024 +0100
@@ -74,7 +74,7 @@
         val s =
           XML.content(Pretty.formatted(content,
             margin = options.int("graphview_content_margin").toDouble,
-            metric = metrics.Pretty_Metric))
+            metric = metrics))
         if (s.nonEmpty) s else node.toString
       }
       else node.toString
@@ -134,7 +134,7 @@
   }
 
   def paint(gfx: Graphics2D): Unit = {
-    gfx.setRenderingHints(Metrics.rendering_hints)
+    gfx.setRenderingHints(Font_Metric.default_hints)
 
     for (node <- graphview.current_node)
       Shapes.highlight_node(gfx, graphview, node)