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