src/Pure/System/message_channel.ML
changeset 54396 8baee6b04a7c
parent 52800 1baa5d19ac44
child 56333 38f1422ef473