src/Pure/PIDE/yxml.scala
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Mon, 17 May 2021 13:40:01 +0200 wenzelm clarified signature;
Sat, 10 Apr 2021 21:50:59 +0200 wenzelm more robust treatment of empty markup: it allows to produce formal chunks;
less more (0) -10 -3 tip