# HG changeset patch
# User wenzelm
# Date 1273264693 -7200
# Node ID 17fe629da5954f87f2673b7f460235f1d2b93421
# Parent  93753a8c955081a0575f61481c702534825c5857
sidekick: unformatted content, notably without newlines;

diff -r 93753a8c9550 -r 17fe629da595 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri May 07 22:27:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri May 07 22:38:13 2010 +0200
@@ -47,7 +47,7 @@
         for ((command, command_start) <- document.command_range(0) if !stopped) {
           root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
               {
-                val content = command.source(node.start, node.stop)
+                val content = Pretty.str_of(List(XML.Text(command.source(node.start, node.stop))))
                 val id = command.id
 
                 new DefaultMutableTreeNode(new IAsset {