src/Pure/PIDE/command.ML
changeset 65251 4b0a43afc3fb
parent 64677 8dc24130e8fe
child 65948 de7888573ed7