src/Tools/jEdit/src/rendering.scala
changeset 52980 28f59ca8ce78
parent 52900 d29bf6db8a2d
child 53230 6589ff56cc3c
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 12 15:09:13 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 12 17:11:27 2013 +0200
     1.3 @@ -199,15 +199,16 @@
     1.4  
     1.5    private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH)
     1.6  
     1.7 -  def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
     1.8 +  def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
     1.9    {
    1.10 -    snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include), _ =>
    1.11 +    snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]](
    1.12 +      range, Nil, Some(hyperlink_include), _ =>
    1.13          {
    1.14            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
    1.15            if Path.is_ok(name) =>
    1.16              val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    1.17 -            val link = Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0))
    1.18 -            Some(link :: links)
    1.19 +            val link = PIDE.editor.hyperlink_file(jedit_file)
    1.20 +            Some(Text.Info(snapshot.convert(info_range), link) :: links)
    1.21  
    1.22            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    1.23            if !props.exists(
    1.24 @@ -220,23 +221,16 @@
    1.25                  Isabelle_System.source_file(Path.explode(name)) match {
    1.26                    case Some(path) =>
    1.27                      val jedit_file = Isabelle_System.platform_path(path)
    1.28 -                    val link =
    1.29 -                      Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0))
    1.30 -                    Some(link :: links)
    1.31 +                    val link = PIDE.editor.hyperlink_file(jedit_file, line)
    1.32 +                    Some(Text.Info(snapshot.convert(info_range), link) :: links)
    1.33                    case None => None
    1.34                  }
    1.35  
    1.36                case Position.Def_Id_Offset(id, offset) =>
    1.37                  snapshot.state.find_command(snapshot.version, id) match {
    1.38                    case Some((node, command)) =>
    1.39 -                    val sources =
    1.40 -                      node.commands.iterator.takeWhile(_ != command).map(_.source) ++
    1.41 -                        Iterator.single(command.source(Text.Range(0, command.decode(offset))))
    1.42 -                    val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
    1.43 -                    val link =
    1.44 -                      Text.Info(snapshot.convert(info_range),
    1.45 -                        Hyperlink(command.node_name.node, line, column))
    1.46 -                    Some(link :: links)
    1.47 +                    PIDE.editor.hyperlink_command(snapshot, command, offset)
    1.48 +                      .map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
    1.49                    case None => None
    1.50                  }
    1.51