src/Pure/PIDE/xml.scala
Thu, 27 Jun 2024 23:18:28 +0200 wenzelm clarified treatment of empty markup;
Thu, 27 Jun 2024 22:39:20 +0200 wenzelm more robust: prefer tail-recursive traversal;
Thu, 27 Jun 2024 22:09:09 +0200 wenzelm clarified signature: more explicit types;
less more (0) -30 -10 -3 tip