src/Pure/General/json.scala
Tue, 21 Apr 2020 22:04:15 +0200 wenzelm clarified signature -- avoid warning;
Fri, 27 Mar 2020 22:01:27 +0100 wenzelm misc tuning based on hints by IntelliJ IDEA;
less more (0) -10 -2 tip