changeset 59713 | 6da3efec20ca |
parent 59708 | aed304412e43 |
child 59715 | 4f0d0e4ad68d |
--- a/src/Pure/PIDE/command.scala Sun Mar 15 23:46:00 2015 +0100 +++ b/src/Pure/PIDE/command.scala Mon Mar 16 11:07:56 2015 +0100 @@ -234,7 +234,7 @@ if (Protocol.is_inlined(message)) { for { (chunk_name, chunk) <- command.chunks.iterator - range <- Protocol.message_positions( + range <- Protocol_Message.positions( self_id, command.position, chunk_name, chunk, message) } st = st.add_markup(false, chunk_name, Text.Info(range, message2)) }