src/Pure/PIDE/document.ML
changeset 64614 88211daacf93
parent 63022 785a59235a15
child 65357 9a2c266f97c8