src/Pure/PIDE/command.ML
changeset 78694 5e995ceb7490
parent 78681 38fe769658be
child 78705 fde0b195cb7d