src/Tools/Graphview/shapes.scala
Sat, 09 Apr 2022 15:40:29 +0200 wenzelm more robust: avoid partiality;
Sat, 09 Apr 2022 14:29:34 +0200 wenzelm clarified signature;
Sat, 09 Apr 2022 12:02:38 +0200 wenzelm avoid pattern-match warnings, notably in scala3;
Sat, 09 Apr 2022 11:56:48 +0200 wenzelm proper type conversion for scala-2.13: problem was unnoticed since ca17e9ebfdf1;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Thu, 04 Mar 2021 15:41:46 +0100 wenzelm tuned --- fewer warnings;
Mon, 01 Mar 2021 22:22:12 +0100 wenzelm tuned --- fewer warnings;
Sat, 02 Apr 2016 14:17:03 +0200 wenzelm more robust display of bidirectional Unicode text: enforce left-to-right;
Sun, 03 May 2015 00:01:10 +0200 wenzelm misc tuning, based on warnings by IntelliJ IDEA;
Wed, 28 Jan 2015 19:15:13 +0100 wenzelm clarified module name;
Mon, 19 Jan 2015 21:06:01 +0100 wenzelm tuned colors;
Mon, 19 Jan 2015 16:38:01 +0100 wenzelm clarified edge_color;
Sat, 17 Jan 2015 22:20:57 +0100 wenzelm more explicit Layout.Info: size and content;
Tue, 06 Jan 2015 16:41:31 +0100 wenzelm tuned signature;
Tue, 06 Jan 2015 16:33:30 +0100 wenzelm explict layout graph structure, with dummies and coordinates;
less more (0) -15 tip