src/Pure/PIDE/query_operation.scala
changeset 64086 ac7ae5067783
parent 63805 c272680df665
child 64664 951507563033
equal deleted inserted replaced
64085:1c451e5c145f 64086:ac7ae5067783