hyperlink for visible positions;
authorwenzelm
Mon Feb 17 20:54:03 2014 +0100 (2014-02-17 ago)
changeset 555474a9f76263ece
parent 55546 cf1baba89a27
child 55548 76979adf0b96
hyperlink for visible positions;
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Feb 17 20:19:02 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Feb 17 20:54:03 2014 +0100
     1.3 @@ -258,7 +258,21 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.URL)
     1.8 +  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
     1.9 +
    1.10 +  private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
    1.11 +    if (Path.is_ok(name))
    1.12 +      Isabelle_System.source_file(Path.explode(name)).map(path =>
    1.13 +        PIDE.editor.hyperlink_file(Isabelle_System.platform_path(path), line))
    1.14 +    else None
    1.15 +
    1.16 +  private def hyperlink_command(id: Document_ID.Generic, offset: Text.Offset)
    1.17 +      : Option[PIDE.editor.Hyperlink] =
    1.18 +    snapshot.state.find_command(snapshot.version, id) match {
    1.19 +      case Some((node, command)) =>
    1.20 +        PIDE.editor.hyperlink_command(snapshot, command, offset)
    1.21 +      case None => None
    1.22 +    }
    1.23  
    1.24    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    1.25    {
    1.26 @@ -281,26 +295,22 @@
    1.27                case (Markup.KIND, Markup.ML_STRUCT) => true
    1.28                case _ => false }) =>
    1.29  
    1.30 -            props match {
    1.31 -              case Position.Def_Line_File(line, name) if Path.is_ok(name) =>
    1.32 -                Isabelle_System.source_file(Path.explode(name)) match {
    1.33 -                  case Some(path) =>
    1.34 -                    val jedit_file = Isabelle_System.platform_path(path)
    1.35 -                    val link = PIDE.editor.hyperlink_file(jedit_file, line)
    1.36 -                    Some(Text.Info(snapshot.convert(info_range), link) :: links)
    1.37 -                  case None => None
    1.38 -                }
    1.39 +            val opt_link =
    1.40 +              props match {
    1.41 +                case Position.Def_Line_File(line, name) => hyperlink_file(line, name)
    1.42 +                case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset)
    1.43 +                case _ => None
    1.44 +              }
    1.45 +            opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
    1.46  
    1.47 -              case Position.Def_Id_Offset(id, offset) =>
    1.48 -                snapshot.state.find_command(snapshot.version, id) match {
    1.49 -                  case Some((node, command)) =>
    1.50 -                    PIDE.editor.hyperlink_command(snapshot, command, offset)
    1.51 -                      .map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
    1.52 -                  case None => None
    1.53 -                }
    1.54 -
    1.55 -              case _ => None
    1.56 -            }
    1.57 +          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    1.58 +            val opt_link =
    1.59 +              props match {
    1.60 +                case Position.Line_File(line, name) => hyperlink_file(line, name)
    1.61 +                case Position.Id_Offset(id, offset) => hyperlink_command(id, offset)
    1.62 +                case _ => None
    1.63 +              }
    1.64 +            opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
    1.65  
    1.66            case _ => None
    1.67          }) match { case Text.Info(_, info :: _) :: _ => Some(info) case _ => None }