equal
deleted
inserted
replaced
128 import Isabelle_Sidekick.int_to_pos |
128 import Isabelle_Sidekick.int_to_pos |
129 |
129 |
130 val root = data.root |
130 val root = data.root |
131 val document = model.recent_document() |
131 val document = model.recent_document() |
132 for ((command, command_start) <- document.command_range(0) if !stopped) { |
132 for ((command, command_start) <- document.command_range(0) if !stopped) { |
133 root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) => |
133 root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) => |
134 { |
134 { |
135 val content = command.source(node.start, node.stop).replace('\n', ' ') |
135 val content = command.source(node.start, node.stop).replace('\n', ' ') |
136 val id = command.id |
136 val id = command.id |
137 |
137 |
138 new DefaultMutableTreeNode(new IAsset { |
138 new DefaultMutableTreeNode(new IAsset { |