src/Pure/PIDE/session.ML
changeset 59697 43e14b0e2ef8
parent 59448 149d2bc5ddb6
child 60081 9fb7b44e3e7e