# HG changeset patch
# User wenzelm
# Date 1375438769 -7200
# Node ID 9489ca1d55dd714dd51d4f2e29fad887c280f4b1
# Parent  820339715ffe79f32ca2dae35837871ad0579d62
some tracking of command location;
tuned;

diff -r 820339715ffe -r 9489ca1d55dd src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 12:17:55 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 12:19:29 2013 +0200
@@ -57,11 +57,30 @@
   private def apply_query(text: String)
   {
     Swing_Thread.require()
+
+    Document_View(view.getTextArea) match {
+      case Some(doc_view) =>
+        val snapshot = doc_view.model.snapshot()
+        current_location = snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1)
+      case None =>
+    }
   }
 
   private def locate_query()
   {
     Swing_Thread.require()
+
+    current_location match {
+      case Some(command) =>
+        val snapshot = PIDE.session.snapshot(command.node_name)
+        val commands = snapshot.node.commands
+        if (commands.contains(command)) {
+          val sources = commands.iterator.takeWhile(_ != command).map(_.source)
+          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
+          Hyperlink(command.node_name.node, line, column).follow(view)
+        }
+      case None =>
+    }
   }
 
 
@@ -90,7 +109,7 @@
 
     PIDE.session.global_options += main_actor
     PIDE.session.commands_changed += main_actor
-    handle_output()
+    handle_resize()
   }
 
   override def exit()