src/Pure/GUI/font_metric.scala
Mon, 04 Nov 2024 21:54:34 +0100 wenzelm support value-oriented Font_Metric, e.g. for caching Pretty output;
Mon, 04 Nov 2024 21:25:26 +0100 wenzelm tuned;
Mon, 04 Nov 2024 21:05:05 +0100 wenzelm tuned;
Mon, 04 Nov 2024 20:55:01 +0100 wenzelm clarified signature;
less more (0) tip