src/Pure/PIDE/query_operation.scala
changeset 76853 e37c58cbb79f
parent 76680 e95b9c9e17ff
child 78592 fdfe9b91d96e
equal deleted inserted replaced
76852:2915740fce1f 76853:e37c58cbb79f