src/Pure/PIDE/document.ML
changeset 71960 6a64205b491a
parent 71674 48ff625687f5
child 72747 5f9d66155081
equal deleted inserted replaced
71958:4320875eb8a1 71960:6a64205b491a