--- a/src/Pure/PIDE/rendering.scala Fri Jan 20 19:52:52 2023 +0100
+++ b/src/Pure/PIDE/rendering.scala Fri Jan 20 20:26:42 2023 +0100
@@ -155,7 +155,6 @@
val tooltip_descriptions =
Map(
- Markup.CITATION -> "citation",
Markup.TOKEN_RANGE -> "inner syntax token",
Markup.FREE -> "free variable",
Markup.SKOLEM -> "skolem variable",
@@ -207,8 +206,6 @@
val language_elements = Markup.Elements(Markup.LANGUAGE)
- val citation_elements = Markup.Elements(Markup.CITATION)
-
val active_elements =
Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.THEORY_EXPORTS,
Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
@@ -320,14 +317,6 @@
Some(Completion.Language_Context.inner)
}).headOption.map(_.info)
- def citations(range: Text.Range): List[Text.Info[String]] =
- snapshot.select(range, Rendering.citation_elements, _ =>
- {
- case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
- Some(Text.Info(snapshot.convert(info_range), name))
- case _ => None
- }).map(_.info)
-
/* file-system path completion */