more precise navigation within open files;
authorwenzelm
Mon Mar 03 11:37:06 2014 +0100 (2014-03-03 ago)
changeset 558786d092a5166f1
parent 55877 65c9968286d5
child 55879 ac979f750c1a
more precise navigation within open files;
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 10:59:33 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 11:37:06 2014 +0100
     1.3 @@ -178,11 +178,30 @@
     1.4    def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
     1.5      new Hyperlink { def follow(view: View) = goto_file(view, name, line, column) }
     1.6  
     1.7 -  def hyperlink_source_file(name: String, line: Int): Option[Hyperlink] =
     1.8 -    if (Path.is_ok(name))
     1.9 -      Isabelle_System.source_file(Path.explode(name)).map(path =>
    1.10 -        hyperlink_file(Isabelle_System.platform_path(path), line))
    1.11 +  def hyperlink_source_file(source_name: String, line: Int, raw_offset: Text.Offset)
    1.12 +    : Option[Hyperlink] =
    1.13 +  {
    1.14 +    if (Path.is_ok(source_name)) {
    1.15 +      Isabelle_System.source_file(Path.explode(source_name)) match {
    1.16 +        case Some(path) =>
    1.17 +          val name = Isabelle_System.platform_path(path)
    1.18 +          JEdit_Lib.jedit_buffer(name) match {
    1.19 +            case Some(buffer) if raw_offset > 0 =>
    1.20 +              val (line, column) =
    1.21 +                JEdit_Lib.buffer_lock(buffer) {
    1.22 +                  ((1, 1) /:
    1.23 +                    (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
    1.24 +                      zipWithIndex.takeWhile(p => p._2 < raw_offset - 1).map(_._1)))(
    1.25 +                        Symbol.advance_line_column)
    1.26 +                }
    1.27 +              Some(hyperlink_file(name, line, column))
    1.28 +            case _ => Some(hyperlink_file(name, line))
    1.29 +          }
    1.30 +        case None => None
    1.31 +      }
    1.32 +    }
    1.33      else None
    1.34 +  }
    1.35  
    1.36    def hyperlink_url(name: String): Hyperlink =
    1.37      new Hyperlink {
     2.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 10:59:33 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 11:37:06 2014 +0100
     2.3 @@ -330,7 +330,8 @@
     2.4    private def hyperlink_file(props: Properties.T): Option[PIDE.editor.Hyperlink] =
     2.5      props match {
     2.6        case Position.Def_Line_File(line, name) =>
     2.7 -        PIDE.editor.hyperlink_source_file(name, line)
     2.8 +        val offset = Position.Def_Offset.unapply(props) getOrElse 0
     2.9 +        PIDE.editor.hyperlink_source_file(name, line, offset)
    2.10        case Position.Def_Id_Offset(id, offset) =>
    2.11          PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    2.12        case _ => None