--- a/src/Tools/jEdit/src/jedit_rendering.scala Sat Mar 30 20:54:47 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Sat Mar 30 22:51:38 2019 +0100
@@ -124,8 +124,8 @@
Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
private val hyperlink_elements =
- Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.POSITION,
- Markup.CITATION)
+ Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.EXPORT_PATH, Markup.DOC, Markup.URL,
+ Markup.POSITION, Markup.CITATION)
private val gutter_elements =
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
@@ -242,6 +242,10 @@
val link = PIDE.editor.hyperlink_file(true, file)
Some(links :+ Text.Info(snapshot.convert(info_range), link))
+ case (links, Text.Info(info_range, XML.Elem(Markup.Export_Path(name), _))) =>
+ val link = PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name)
+ Some(links :+ Text.Info(snapshot.convert(info_range), link))
+
case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>
PIDE.editor.hyperlink_doc(name).map(link =>
(links :+ Text.Info(snapshot.convert(info_range), link)))