src/Pure/PIDE/document.ML
changeset 41171 043f8dc3b51f
parent 40534 9e196062bf88
child 41537 3837045cc8a1