src/Tools/jEdit/src/jedit_editor.scala
changeset 56458 a8d960baa5c2
parent 56457 eea4bbe15745
child 56461 ae33d153f6cc
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 07 21:23:02 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 07 23:02:29 2014 +0200
     1.3 @@ -195,26 +195,32 @@
     1.4    def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
     1.5      : Option[Hyperlink] =
     1.6    {
     1.7 -    if (Path.is_valid(source_name)) {
     1.8 -      Isabelle_System.source_file(Path.explode(source_name)) match {
     1.9 -        case Some(path) =>
    1.10 -          val name = Isabelle_System.platform_path(path)
    1.11 -          JEdit_Lib.jedit_buffer(name) match {
    1.12 -            case Some(buffer) if offset > 0 =>
    1.13 -              val (line, column) =
    1.14 -                JEdit_Lib.buffer_lock(buffer) {
    1.15 -                  ((1, 1) /:
    1.16 -                    (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
    1.17 -                      zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
    1.18 -                        Symbol.advance_line_column)
    1.19 -                }
    1.20 -              Some(hyperlink_file(name, line, column))
    1.21 -            case _ => Some(hyperlink_file(name, line))
    1.22 -          }
    1.23 -        case None => None
    1.24 +    val opt_name =
    1.25 +      if (Path.is_wellformed(source_name)) {
    1.26 +        if (Path.is_valid(source_name)) {
    1.27 +          val path = Path.explode(source_name)
    1.28 +          Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
    1.29 +        }
    1.30 +        else None
    1.31        }
    1.32 +      else Some(source_name)
    1.33 +
    1.34 +    opt_name match {
    1.35 +      case Some(name) =>
    1.36 +        JEdit_Lib.jedit_buffer(name) match {
    1.37 +          case Some(buffer) if offset > 0 =>
    1.38 +            val (line, column) =
    1.39 +              JEdit_Lib.buffer_lock(buffer) {
    1.40 +                ((1, 1) /:
    1.41 +                  (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
    1.42 +                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
    1.43 +                      Symbol.advance_line_column)
    1.44 +              }
    1.45 +            Some(hyperlink_file(name, line, column))
    1.46 +          case _ => Some(hyperlink_file(name, line))
    1.47 +        }
    1.48 +      case None => None
    1.49      }
    1.50 -    else None
    1.51    }
    1.52  
    1.53    def hyperlink_url(name: String): Hyperlink =