diff -r 5b0003211207 -r 6da3efec20ca src/Pure/PIDE/command.scala --- 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)) }