src/Pure/PIDE/document.ML
changeset 48803 ffa31bf5c662
parent 48772 e46cd0d26481
child 48918 6e5fd4585512