src/Pure/PIDE/protocol.ML
changeset 48754 c2c1e5944536
parent 48707 ba531af91148
child 48755 393a37003851