src/Pure/PIDE/document.ML
changeset 57916 2c2c24dbf0a4
parent 57905 c0c5652e796e
child 57918 f5d73caba4e5