src/Tools/jEdit/src/jedit_rendering.scala

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sun Jan 13 19:03:16 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sun Jan 13 19:42:06 2019 +0100
@@ -118,14 +118,14 @@
 
   private val highlight_elements =
     Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
-      Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
-      Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
-      Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
+      Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.THEORY_EXPORTS,
+      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM,
+      Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
       Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
 
   private val hyperlink_elements =
-    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION,
-      Markup.CITATION, Markup.URL)
+    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.THEORY_EXPORTS,
+      Markup.POSITION, Markup.CITATION)
 
   private val gutter_elements =
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
@@ -250,6 +250,10 @@
             val link = PIDE.editor.hyperlink_url(name)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
+          case (links, Text.Info(info_range, XML.Elem(Markup.Theory_Exports(name), _))) =>
+            val link = PIDE.editor.hyperlink_theory_exports(name)
+            Some(links :+ Text.Info(snapshot.convert(info_range), link))
+
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
             val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))