src/Pure/PIDE/document.ML
changeset 58215 cccf5445e224
parent 57918 f5d73caba4e5
child 58903 38c72f5f6c2e