src/Pure/PIDE/document.ML
changeset 69920 79c8ff387ed1
parent 69886 0cb8753bdb50
child 70282 242c50877dd2