src/Pure/GUI/rich_text.scala
changeset 82026 57b4e44f5bc4
parent 81433 c3793899b880
child 82229 ac7c09c6ff2f
equal deleted inserted replaced
82017:9a8d408492a7 82026:57b4e44f5bc4