src/Pure/PIDE/document.ML
changeset 67651 6dd41193a72a
parent 67500 dfde99d59f6e
child 68184 6c693b2700b3
equal deleted inserted replaced
67650:5e4f9a0ffea5 67651:6dd41193a72a