# HG changeset patch
# User wenzelm
# Date 1326146913 -3600
# Node ID a01c969f2e143bf854e714d1c4b9f9656f172321
# Parent  6c880b26dfc43940d040ef39949beaa0c6004f52
tuned;

diff -r 6c880b26dfc4 -r a01c969f2e14 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Jan 09 18:33:55 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Jan 09 23:08:33 2012 +0100
@@ -34,8 +34,7 @@
           (this /: msgs)((state, msg) =>
             msg match {
               case elem @ XML.Elem(markup, Nil) =>
-                val info: Text.Markup = Text.Info(command.range, elem)
-                state.add_status(markup).add_markup(info)
+                state.add_status(markup).add_markup(Text.Info(command.range, elem))
 
               case _ => System.err.println("Ignored status message: " + msg); state
             })