src/Tools/jEdit/src/isabelle_hyperlinks.scala
changeset 45474 f793dd5d84b2
parent 45468 33e946d3f449
child 45666 d83797ef0d2d
     1.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Sat Nov 12 18:56:49 2011 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Sat Nov 12 19:44:56 2011 +0100
     1.3 @@ -89,7 +89,8 @@
     1.4                          }
     1.5                        case _ => null
     1.6                      }
     1.7 -                }))
     1.8 +                },
     1.9 +                Some(Set(Markup.ENTITY))))
    1.10            markup match {
    1.11              case Text.Info(_, Some(link)) #:: _ => link
    1.12              case _ => null