# HG changeset patch
# User wenzelm
# Date 1282675008 -7200
# Node ID 20d82e98bcd72697219d2c3525be548273b7c934
# Parent  2e0ebdaac59b0e4ffc8727f077200777dfa0fb97
tuned root markup;

diff -r 2e0ebdaac59b -r 20d82e98bcd7 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Aug 23 20:50:00 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 24 20:36:48 2010 +0200
@@ -26,10 +26,10 @@
 
     def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
 
-    def markup_root_info: Text.Info[Any] =
+    def root_info: Text.Info[Any] =
       new Text.Info(command.range,
-        XML.Elem(Markup(Markup.STATUS, Nil), status.map(XML.Elem(_, Nil))))
-    def markup_root: Markup_Tree = markup + markup_root_info
+        XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
+    def root_markup: Markup_Tree = markup + root_info
 
 
     /* message dispatch */
diff -r 2e0ebdaac59b -r 20d82e98bcd7 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Mon Aug 23 20:50:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Aug 24 20:36:48 2010 +0200
@@ -130,7 +130,7 @@
     val root = data.root
     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
-      snapshot.state(command).markup_root.swing_tree(root)((info: Text.Info[Any]) =>
+      snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
           {
             val content = command.source(info.range).replace('\n', ' ')
             val id = command.id