src/Pure/PIDE/xml.scala
Thu, 10 Oct 2019 16:51:47 +0200 wenzelm more compact XML representation;
less more (0) -30 -10 -1 tip