--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Apr 04 18:06:48 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Apr 04 18:20:00 2013 +0200
@@ -44,6 +44,16 @@
override def setEnd(end: Position) = _end = end
override def toString = _name
}
+
+ def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
+ swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
+ {
+ for ((_, entry) <- tree.branches) {
+ val node = swing_node(Text.Info(entry.range, entry.markup))
+ swing_markup_tree(entry.subtree, node, swing_node)
+ parent.add(node)
+ }
+ }
}
@@ -195,8 +205,9 @@
case Some(snapshot) =>
val root = data.root
for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
- snapshot.state.command_state(snapshot.version, command).markup
- .swing_tree(root, (info: Text.Info[List[XML.Elem]]) =>
+ Isabelle_Sidekick.swing_markup_tree(
+ snapshot.state.command_state(snapshot.version, command).markup, root,
+ (info: Text.Info[List[XML.Elem]]) =>
{
val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')