--- a/src/Tools/Graphview/metrics.scala Mon Nov 04 21:05:05 2024 +0100 +++ b/src/Tools/Graphview/metrics.scala Mon Nov 04 21:05:11 2024 +0100 @@ -10,7 +10,6 @@ import isabelle._ import java.awt.Font -import java.awt.geom.Rectangle2D object Metrics {