--- a/src/Pure/PIDE/editor.scala Fri Jan 20 19:52:52 2023 +0100
+++ b/src/Pure/PIDE/editor.scala Fri Jan 20 20:26:42 2023 +0100
@@ -17,16 +17,6 @@
def get_models(): Iterable[Document.Model]
- /* bibtex */
-
- def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document.Model)]] =
- Bibtex.Entries.iterator(get_models())
-
- def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
- : Option[Completion.Result] =
- Bibtex.completion(history, rendering, caret, get_models())
-
-
/* document editor */
protected val document_editor: Synchronized[Document_Editor.State] =
--- 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 */
--- a/src/Pure/Thy/bibtex.ML Fri Jan 20 19:52:52 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML Fri Jan 20 20:26:42 2023 +0100
@@ -75,10 +75,7 @@
fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) =
let
val loc = the_default Input.empty opt_loc;
- val _ =
- Context_Position.reports ctxt
- (Document_Output.document_reports loc @
- map (fn (name, pos) => (pos, Markup.citation name)) citations);
+ val _ = Context_Position.reports ctxt (Document_Output.document_reports loc);
val _ = List.app (check_bibtex_entry ctxt) citations;
val kind = if macro_name = "" then get_kind ctxt else macro_name;
--- a/src/Pure/Thy/bibtex.scala Fri Jan 20 19:52:52 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala Fri Jan 20 20:26:42 2023 +0100
@@ -194,13 +194,6 @@
}
catch { case ERROR(msg) => apply(Nil, errors = List(msg)) }
}
-
- def iterator[A <: Document.Model](models: Iterable[A]): Iterator[Text.Info[(String, A)]] =
- for {
- model <- models.iterator
- bibtex_entries <- model.get_data(classOf[Entries]).iterator
- info <- bibtex_entries.entries.iterator
- } yield info.map((_, model))
}
final class Entries private(val entries: List[Text.Info[String]], val errors: List[String]) {
@@ -229,40 +222,6 @@
}
- /* completion */
-
- def completion[A <: Document.Model](
- history: Completion.History,
- rendering: Rendering,
- caret: Text.Offset,
- models: Iterable[A]
- ): Option[Completion.Result] = {
- for {
- Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption
- name1 <- Completion.clean_name(name)
-
- original <- rendering.get_text(r)
- original1 <- Completion.clean_name(Library.perhaps_unquote(original))
-
- entries =
- (for {
- Text.Info(_, (entry, _)) <- Entries.iterator(models)
- if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1
- } yield entry).toList
- if entries.nonEmpty
-
- items =
- entries.sorted.map({
- case entry =>
- val full_name = Long_Name.qualify(Markup.CITATION, entry)
- val description = List(entry, "(BibTeX entry)")
- val replacement = quote(entry)
- Completion.Item(r, original, full_name, description, replacement, 0, false)
- }).sorted(history.ordering).take(rendering.options.int("completion_limit"))
- } yield Completion.Result(r, original, false, items)
- }
-
-
/** content **/
--- a/src/Pure/Thy/sessions.scala Fri Jan 20 19:52:52 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Jan 20 20:26:42 2023 +0100
@@ -996,14 +996,6 @@
def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss)
def imports_topological_order: List[String] = imports_graph.topological_order
- def bibtex_entries: List[(String, List[String])] =
- build_topological_order.flatMap { name =>
- apply(name).bibtex_entries.entries match {
- case Nil => None
- case entries => Some(name -> entries.map(_.info))
- }
- }
-
override def toString: String =
imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
}
--- a/src/Tools/Haskell/Haskell.thy Fri Jan 20 19:52:52 2023 +0100
+++ b/src/Tools/Haskell/Haskell.thy Fri Jan 20 20:26:42 2023 +0100
@@ -737,8 +737,6 @@
expressionN, expression,
- citationN, citation,
-
pathN, path, urlN, url, docN, doc,
markupN, consistentN, unbreakableN, indentN, widthN,
@@ -905,14 +903,6 @@
expression kind = (expressionN, if kind == "" then [] else [(kindN, kind)])
-{- citation -}
-
-citationN :: Bytes
-citationN = \<open>Markup.citationN\<close>
-citation :: Bytes -> T
-citation = markup_string nameN citationN
-
-
{- external resources -}
pathN :: Bytes
--- a/src/Tools/VSCode/src/vscode_rendering.scala Fri Jan 20 19:52:52 2023 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Fri Jan 20 20:26:42 2023 +0100
@@ -63,7 +63,7 @@
Rendering.tooltip_elements
private val hyperlink_elements =
- Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
+ Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION)
}
class VSCode_Rendering(snapshot: Document.Snapshot, val model: VSCode_Model)
@@ -104,8 +104,7 @@
semantic_completion,
syntax_completion,
VSCode_Spell_Checker.completion(rendering, caret),
- path_completion(caret),
- model.editor.bibtex_completion(history, rendering, caret))
+ path_completion(caret))
val items =
results match {
case None => Nil
@@ -311,15 +310,6 @@
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
hyperlink_position(props).map(_ :: links)
- case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
- val iterator =
- for {
- Text.Info(entry_range, (entry, model: VSCode_Model)) <-
- model.editor.bibtex_entries_iterator()
- if entry == name
- } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
- if (iterator.isEmpty) None else Some(iterator.foldLeft(links)(_ :+ _))
-
case _ => None
}) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
}
--- a/src/Tools/jEdit/src/completion_popup.scala Fri Jan 20 19:52:52 2023 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Jan 20 20:26:42 2023 +0100
@@ -121,8 +121,7 @@
val range0 =
Completion.Result.merge(Completion.History.empty,
syntax_completion(Completion.History.empty, true, Some(rendering)),
- rendering.path_completion(caret),
- PIDE.editor.bibtex_completion(Completion.History.empty, rendering, caret))
+ rendering.path_completion(caret))
.map(_.range)
rendering.semantic_completion(range0, range) match {
case None => range0
@@ -303,8 +302,7 @@
Completion.Result.merge(history,
result1,
JEdit_Spell_Checker.completion(rendering, explicit, caret),
- rendering.path_completion(caret),
- PIDE.editor.bibtex_completion(history, rendering, caret))
+ rendering.path_completion(caret))
}
}
result match {
--- a/src/Tools/jEdit/src/jedit_rendering.scala Fri Jan 20 19:52:52 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Fri Jan 20 20:26:42 2023 +0100
@@ -127,7 +127,7 @@
private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
private val highlight_elements =
- Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
+ Markup.Elements(Markup.EXPRESSION, 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,
@@ -135,7 +135,7 @@
private val hyperlink_elements =
Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.EXPORT_PATH, Markup.DOC, Markup.URL,
- Markup.POSITION, Markup.CITATION)
+ Markup.POSITION)
private val gutter_elements =
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
@@ -270,13 +270,6 @@
val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
- case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
- val opt_link =
- PIDE.editor.bibtex_entries_iterator().collectFirst(
- { case Text.Info(entry_range, (entry, model: Document_Model)) if entry == name =>
- PIDE.editor.hyperlink_model(true, model, entry_range.start) })
- opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
-
case _ => None
}) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
}