src/Pure/PIDE/document.ML
changeset 78271 c0dc000d2a40
parent 77723 b761c91c2447
child 78489 40d50936484c