src/Pure/PIDE/document.ML
changeset 58227 d91f7a80f412
parent 57918 f5d73caba4e5
child 58903 38c72f5f6c2e