src/Pure/PIDE/document.ML
changeset 69145 806be481aa57
parent 68869 3739acbc2178
child 69826 1bea05713dde