src/Pure/PIDE/query_operation.ML
changeset 80389 5e8dca75c699
parent 78757 a094bf81a496
child 80826 7feaa04d332b