src/Pure/PIDE/document.ML
changeset 64494 979520c83f30
parent 63022 785a59235a15
child 65357 9a2c266f97c8