# HG changeset patch
# User wenzelm
# Date 1393843026 -3600
# Node ID 6d092a5166f1897ce771049b247e00df88f49a6c
# Parent  65c9968286d54a0be9456fcf96f484c5d345ec78
more precise navigation within open files;

diff -r 65c9968286d5 -r 6d092a5166f1 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 10:59:33 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 11:37:06 2014 +0100
@@ -178,11 +178,30 @@
   def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
     new Hyperlink { def follow(view: View) = goto_file(view, name, line, column) }
 
-  def hyperlink_source_file(name: String, line: Int): Option[Hyperlink] =
-    if (Path.is_ok(name))
-      Isabelle_System.source_file(Path.explode(name)).map(path =>
-        hyperlink_file(Isabelle_System.platform_path(path), line))
+  def hyperlink_source_file(source_name: String, line: Int, raw_offset: Text.Offset)
+    : Option[Hyperlink] =
+  {
+    if (Path.is_ok(source_name)) {
+      Isabelle_System.source_file(Path.explode(source_name)) match {
+        case Some(path) =>
+          val name = Isabelle_System.platform_path(path)
+          JEdit_Lib.jedit_buffer(name) match {
+            case Some(buffer) if raw_offset > 0 =>
+              val (line, column) =
+                JEdit_Lib.buffer_lock(buffer) {
+                  ((1, 1) /:
+                    (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
+                      zipWithIndex.takeWhile(p => p._2 < raw_offset - 1).map(_._1)))(
+                        Symbol.advance_line_column)
+                }
+              Some(hyperlink_file(name, line, column))
+            case _ => Some(hyperlink_file(name, line))
+          }
+        case None => None
+      }
+    }
     else None
+  }
 
   def hyperlink_url(name: String): Hyperlink =
     new Hyperlink {
diff -r 65c9968286d5 -r 6d092a5166f1 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 10:59:33 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 11:37:06 2014 +0100
@@ -330,7 +330,8 @@
   private def hyperlink_file(props: Properties.T): Option[PIDE.editor.Hyperlink] =
     props match {
       case Position.Def_Line_File(line, name) =>
-        PIDE.editor.hyperlink_source_file(name, line)
+        val offset = Position.Def_Offset.unapply(props) getOrElse 0
+        PIDE.editor.hyperlink_source_file(name, line, offset)
       case Position.Def_Id_Offset(id, offset) =>
         PIDE.editor.hyperlink_command_id(snapshot, id, offset)
       case _ => None