src/Pure/System/message_channel.ML
changeset 81310 e3b0c7aec1ed
parent 80505 e3af424fdd1a