src/Pure/PIDE/xml.scala
Thu, 08 Mar 2012 21:36:36 +0100 wenzelm simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);
less more (0) -1 tip