src/Pure/PIDE/command.scala
changeset 38658 20d82e98bcd7
parent 38637 03b27bd0505e
child 38714 31da698fc4e5
     1.1 --- a/src/Pure/PIDE/command.scala	Mon Aug 23 20:50:00 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 24 20:36:48 2010 +0200
     1.3 @@ -26,10 +26,10 @@
     1.4  
     1.5      def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
     1.6  
     1.7 -    def markup_root_info: Text.Info[Any] =
     1.8 +    def root_info: Text.Info[Any] =
     1.9        new Text.Info(command.range,
    1.10 -        XML.Elem(Markup(Markup.STATUS, Nil), status.map(XML.Elem(_, Nil))))
    1.11 -    def markup_root: Markup_Tree = markup + markup_root_info
    1.12 +        XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
    1.13 +    def root_markup: Markup_Tree = markup + root_info
    1.14  
    1.15  
    1.16      /* message dispatch */