sidekick: unformatted content, notably without newlines;
authorwenzelm
Fri, 07 May 2010 22:38:13 +0200
changeset 3673717fe629da595
parent 36736 93753a8c9550
child 36738 dce592144219
sidekick: unformatted content, notably without newlines;
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri May 07 22:27:28 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri May 07 22:38:13 2010 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4          for ((command, command_start) <- document.command_range(0) if !stopped) {
     1.5            root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
     1.6                {
     1.7 -                val content = command.source(node.start, node.stop)
     1.8 +                val content = Pretty.str_of(List(XML.Text(command.source(node.start, node.stop))))
     1.9                  val id = command.id
    1.10  
    1.11                  new DefaultMutableTreeNode(new IAsset {