--- 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 */
--- 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