diff -r 8abdd60acd60 -r 07c802837a8c src/Pure/GUI/tree_view.scala