src/Pure/PIDE/document.ML
changeset 78448 573cc2ab69c5
parent 77723 b761c91c2447
child 78489 40d50936484c