src/Pure/PIDE/command.ML
changeset 66411 72de7d59e2f7
parent 66379 6392766f3c25
child 67184 ecc786cb3b7b