# HG changeset patch
# User wenzelm
# Date 1273403893 -7200
# Node ID 17427cf6fe9506244670ea9dce796cf408a715ca
# Parent  096ebe74aeaf9e4b0bf04b50e38b41f5391b00e2
more basic replacement of newlines;

diff -r 096ebe74aeaf -r 17427cf6fe95 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun May 09 13:12:22 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun May 09 13:18:13 2010 +0200
@@ -132,7 +132,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 = Pretty.str_of(List(XML.Text(command.source(node.start, node.stop))))
+            val content = command.source(node.start, node.stop).replace('\n', ' ')
             val id = command.id
 
             new DefaultMutableTreeNode(new IAsset {