src/Pure/PIDE/document.ML
changeset 66053 cd8d0ad5ac19
parent 65445 e9e7f5f5794c
child 66167 1bd268ab885c