src/Pure/PIDE/document.ML
changeset 76019 f3d8da992445
parent 76013 9ac09016d036
child 76405 aaf307f865c9