src/Pure/PIDE/markup.scala
changeset 61578 6623c81cb15a
parent 61449 4f31f79cf2d1
child 61598 ed4dad8823a4
equal deleted inserted replaced
61577:de7045616fc7 61578:6623c81cb15a