src/Tools/jEdit/src/jedit_editor.scala
changeset 55878 6d092a5166f1
parent 55877 65c9968286d5
child 55879 ac979f750c1a
     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 {