src/Tools/jEdit/src/rendering.scala
changeset 55876 142139457653
parent 55837 154855d9a564
child 55877 65c9968286d5
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 03:13:45 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 10:41:58 2014 +0100
     1.3 @@ -327,20 +327,6 @@
     1.4  
     1.5    /* hyperlinks */
     1.6  
     1.7 -  private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
     1.8 -    if (Path.is_ok(name))
     1.9 -      Isabelle_System.source_file(Path.explode(name)).map(path =>
    1.10 -        PIDE.editor.hyperlink_file(Isabelle_System.platform_path(path), line))
    1.11 -    else None
    1.12 -
    1.13 -  private def hyperlink_command(id: Document_ID.Generic, offset: Text.Offset)
    1.14 -      : Option[PIDE.editor.Hyperlink] =
    1.15 -    snapshot.state.find_command(snapshot.version, id) match {
    1.16 -      case Some((node, command)) =>
    1.17 -        PIDE.editor.hyperlink_command(snapshot, command, offset)
    1.18 -      case None => None
    1.19 -    }
    1.20 -
    1.21    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    1.22    {
    1.23      snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
    1.24 @@ -364,8 +350,10 @@
    1.25  
    1.26              val opt_link =
    1.27                props match {
    1.28 -                case Position.Def_Line_File(line, name) => hyperlink_file(line, name)
    1.29 -                case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset)
    1.30 +                case Position.Def_Line_File(line, name) =>
    1.31 +                  PIDE.editor.hyperlink_source_file(name, line)
    1.32 +                case Position.Def_Id_Offset(id, offset) =>
    1.33 +                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    1.34                  case _ => None
    1.35                }
    1.36              opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    1.37 @@ -373,8 +361,10 @@
    1.38            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    1.39              val opt_link =
    1.40                props match {
    1.41 -                case Position.Line_File(line, name) => hyperlink_file(line, name)
    1.42 -                case Position.Id_Offset(id, offset) => hyperlink_command(id, offset)
    1.43 +                case Position.Line_File(line, name) =>
    1.44 +                  PIDE.editor.hyperlink_source_file(name, line)
    1.45 +                case Position.Id_Offset(id, offset) =>
    1.46 +                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    1.47                  case _ => None
    1.48                }
    1.49              opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))