src/Tools/jEdit/src/theories_dockable.scala
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)