src/Tools/jEdit/src/jedit_rendering.scala
changeset 64660 ef85bb6491b3
parent 64654 31b681e38c70
child 64676 fd2df1ea3bb4
     1.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Fri Dec 23 11:19:28 2016 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Fri Dec 23 11:21:38 2016 +0100
     1.3 @@ -478,11 +478,7 @@
     1.4              val link = PIDE.editor.hyperlink_url(name)
     1.5              Some(links :+ Text.Info(snapshot.convert(info_range), link))
     1.6  
     1.7 -          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
     1.8 -          if !props.exists(
     1.9 -            { case (Markup.KIND, Markup.ML_OPEN) => true
    1.10 -              case (Markup.KIND, Markup.ML_STRUCTURE) => true
    1.11 -              case _ => false }) =>
    1.12 +          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    1.13              val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
    1.14              opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
    1.15