src/Pure/PIDE/xml.scala
Sun, 11 Mar 2018 21:08:47 +0100 wenzelm tuned;
Sun, 11 Mar 2018 15:05:43 +0100 wenzelm convenience to represent XML.Body as single XML.Elem;
less more (0) -30 -10 -2 tip