src/Pure/PIDE/markup.scala
changeset 52731 dacd47a0633f
parent 52697 6fb98a20c349
child 52800 1baa5d19ac44
equal deleted inserted replaced
52730:6bf02eb4ddf7 52731:dacd47a0633f