src/Pure/PIDE/document.ML
changeset 70009 435fb018e8ee
parent 69886 0cb8753bdb50
child 70282 242c50877dd2