137 Markup.ML_STRING, Markup.ML_COMMENT) |
137 Markup.ML_STRING, Markup.ML_COMMENT) |
138 |
138 |
139 private val language_elements = Markup.Elements(Markup.LANGUAGE) |
139 private val language_elements = Markup.Elements(Markup.LANGUAGE) |
140 |
140 |
141 private val highlight_elements = |
141 private val highlight_elements = |
142 Markup.Elements(Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING, |
142 Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING, |
143 Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, |
143 Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, |
144 Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND, |
144 Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND, |
145 Markup.VAR, Markup.TFREE, Markup.TVAR) |
145 Markup.VAR, Markup.TFREE, Markup.TVAR) |
146 |
146 |
147 private val hyperlink_elements = |
147 private val hyperlink_elements = |
148 Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL) |
148 Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION, Markup.URL) |
149 |
149 |
150 private val active_elements = |
150 private val active_elements = |
151 Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, |
151 Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, |
152 Markup.SENDBACK, Markup.SIMP_TRACE_PANEL) |
152 Markup.SENDBACK, Markup.SIMP_TRACE_PANEL) |
153 |
153 |
155 Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD) |
155 Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD) |
156 |
156 |
157 private val tooltip_descriptions = |
157 private val tooltip_descriptions = |
158 Map( |
158 Map( |
159 Markup.EXPRESSION -> "expression", |
159 Markup.EXPRESSION -> "expression", |
|
160 Markup.CITATION -> "citation", |
160 Markup.TOKEN_RANGE -> "inner syntax token", |
161 Markup.TOKEN_RANGE -> "inner syntax token", |
161 Markup.FREE -> "free variable", |
162 Markup.FREE -> "free variable", |
162 Markup.SKOLEM -> "skolem variable", |
163 Markup.SKOLEM -> "skolem variable", |
163 Markup.BOUND -> "bound variable", |
164 Markup.BOUND -> "bound variable", |
164 Markup.VAR -> "schematic variable", |
165 Markup.VAR -> "schematic variable", |
391 PIDE.editor.hyperlink_source_file(name, line, offset) |
392 PIDE.editor.hyperlink_source_file(name, line, offset) |
392 case Position.Id_Offset0(id, offset) => |
393 case Position.Id_Offset0(id, offset) => |
393 PIDE.editor.hyperlink_command_id(snapshot, id, offset) |
394 PIDE.editor.hyperlink_command_id(snapshot, id, offset) |
394 case _ => None |
395 case _ => None |
395 } |
396 } |
|
397 opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) |
|
398 |
|
399 case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) => |
|
400 val opt_link = |
|
401 Bibtex_JEdit.entries_iterator.collectFirst( |
|
402 { case (a, buffer, offset) if a == name => |
|
403 PIDE.editor.hyperlink_buffer(buffer, offset) }) |
396 opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) |
404 opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) |
397 |
405 |
398 case _ => None |
406 case _ => None |
399 }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None } |
407 }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None } |
400 } |
408 } |