src/Pure/PIDE/document.ML
changeset 48754 c2c1e5944536
parent 48735 35c47932584c
child 48755 393a37003851