116 |
116 |
117 private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT) |
117 private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT) |
118 |
118 |
119 private val highlight_elements = |
119 private val highlight_elements = |
120 Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING, |
120 Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING, |
121 Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING, |
121 Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.THEORY_EXPORTS, |
122 Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND, |
122 Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, |
123 Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT, |
123 Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT, |
124 Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) |
124 Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) |
125 |
125 |
126 private val hyperlink_elements = |
126 private val hyperlink_elements = |
127 Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.POSITION, |
127 Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.THEORY_EXPORTS, |
128 Markup.CITATION, Markup.URL) |
128 Markup.POSITION, Markup.CITATION) |
129 |
129 |
130 private val gutter_elements = |
130 private val gutter_elements = |
131 Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) |
131 Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) |
132 |
132 |
133 private val squiggly_elements = |
133 private val squiggly_elements = |
248 |
248 |
249 case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) => |
249 case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) => |
250 val link = PIDE.editor.hyperlink_url(name) |
250 val link = PIDE.editor.hyperlink_url(name) |
251 Some(links :+ Text.Info(snapshot.convert(info_range), link)) |
251 Some(links :+ Text.Info(snapshot.convert(info_range), link)) |
252 |
252 |
|
253 case (links, Text.Info(info_range, XML.Elem(Markup.Theory_Exports(name), _))) => |
|
254 val link = PIDE.editor.hyperlink_theory_exports(name) |
|
255 Some(links :+ Text.Info(snapshot.convert(info_range), link)) |
|
256 |
253 case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => |
257 case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => |
254 val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props) |
258 val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props) |
255 opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) |
259 opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) |
256 |
260 |
257 case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => |
261 case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => |