src/Pure/PIDE/document.ML
changeset 52798 9d3c9862d1dd
parent 52797 0d6f2a87d1a5
child 52808 143f225e50f5