src/Pure/PIDE/document.ML
changeset 69650 c95edf19133b
parent 68869 3739acbc2178
child 69826 1bea05713dde