src/Pure/PIDE/document.ML
changeset 65667 f1c70c7fea12
parent 65445 e9e7f5f5794c
child 66167 1bd268ab885c