src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
changeset 36737 17fe629da595
parent 36015 6111de7c916a
child 36738 dce592144219
equal deleted inserted replaced
36736:93753a8c9550 36737:17fe629da595
    45       case Some(model) =>
    45       case Some(model) =>
    46         val document = model.recent_document()
    46         val document = model.recent_document()
    47         for ((command, command_start) <- document.command_range(0) if !stopped) {
    47         for ((command, command_start) <- document.command_range(0) if !stopped) {
    48           root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
    48           root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
    49               {
    49               {
    50                 val content = command.source(node.start, node.stop)
    50                 val content = Pretty.str_of(List(XML.Text(command.source(node.start, node.stop))))
    51                 val id = command.id
    51                 val id = command.id
    52 
    52 
    53                 new DefaultMutableTreeNode(new IAsset {
    53                 new DefaultMutableTreeNode(new IAsset {
    54                   override def getIcon: Icon = null
    54                   override def getIcon: Icon = null
    55                   override def getShortString: String = content
    55                   override def getShortString: String = content