equal
deleted
inserted
replaced
43 |
43 |
44 Swing_Thread.now { Document_Model(buffer) } match { |
44 Swing_Thread.now { Document_Model(buffer) } match { |
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).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 = 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 { |