src/Pure/PIDE/query_operation.scala
changeset 80266 d52be75ae60b
parent 78595 b0abf5a9dada
equal deleted inserted replaced
80265:cb795bbce540 80266:d52be75ae60b