changeset 52980 | 28f59ca8ce78 |
parent 52973 | d5f7fa1498b7 |
child 53176 | f88635e1c52e |
--- a/src/Tools/jEdit/src/theories_dockable.scala Mon Aug 12 15:09:13 2013 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Aug 12 17:11:27 2013 +0200 @@ -41,7 +41,7 @@ } model.node_required = !model.node_required } } - else if (clicks == 2) Hyperlink(listData(index).node).follow(view) + else if (clicks == 2) PIDE.editor.goto(view, listData(index).node) } case MouseMoved(_, point, _) => val index = peer.locationToIndex(point)