src/Pure/PIDE/command.scala
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))
               }