src/Pure/GUI/rich_text.scala
changeset 81954 6f2bcdfa9a19
parent 81433 c3793899b880
child 82229 ac7c09c6ff2f