src/Pure/PIDE/markup_node.scala
changeset 38558 32ad17fe2b9c
parent 38426 2858ec7b6dd8
child 38478 7766812a01e7
equal deleted inserted replaced
38557:9926c47ad1a1 38558:32ad17fe2b9c