equal
deleted
inserted
replaced
102 } |
102 } |
103 |
103 |
104 |
104 |
105 /* timing view */ |
105 /* timing view */ |
106 |
106 |
107 private val timing_view = new ListView(Nil: List[Entry]) { |
107 private val timing_view = new ListView(List.empty[Entry]) { |
108 listenTo(mouse.clicks) |
108 listenTo(mouse.clicks) |
109 reactions += { |
109 reactions += { |
110 case MouseClicked(_, point, _, clicks, _) if clicks == 2 => |
110 case MouseClicked(_, point, _, clicks, _) if clicks == 2 => |
111 val index = peer.locationToIndex(point) |
111 val index = peer.locationToIndex(point) |
112 if (index >= 0) listData(index).follow(PIDE.session.snapshot()) |
112 if (index >= 0) listData(index).follow(PIDE.session.snapshot()) |