src/Pure/System/message_channel.ML
changeset 58857 b0ccc7e1e7f3
parent 57417 29fe9bac501b
child 59058 a78612c67ec0
equal deleted inserted replaced
58856:4fced55fc5b7 58857:b0ccc7e1e7f3
    49     fun continue timeout =
    49     fun continue timeout =
    50       (case Mailbox.receive timeout mbox of
    50       (case Mailbox.receive timeout mbox of
    51         [] => (flush channel; continue NONE)
    51         [] => (flush channel; continue NONE)
    52       | msgs => received timeout msgs)
    52       | msgs => received timeout msgs)
    53     and received _ (NONE :: _) = flush channel
    53     and received _ (NONE :: _) = flush channel
    54       | received timeout (SOME msg :: rest) =
    54       | received _ (SOME msg :: rest) = (output_message channel msg; received flush_timeout rest)
    55           (output_message channel msg; received flush_timeout rest)
       
    56       | received timeout [] = continue timeout;
    55       | received timeout [] = continue timeout;
    57   in fn () => continue NONE end;
    56   in fn () => continue NONE end;
    58 
    57 
    59 fun make channel =
    58 fun make channel =
    60   if Multithreading.available then
    59   if Multithreading.available then