src/Pure/PIDE/session.ML
changeset 77287 d060545f01a2
parent 76406 40a365360680
child 78020 1a829342a2d3