src/Pure/PIDE/markup_tree.scala
Sun, 30 Dec 2012 20:15:02 +0100 wenzelm ignore markup elements over empty body, which are not well-defined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
less more (0) -30 -10 -1 tip