# HG changeset patch # User wenzelm # Date 1674242802 -3600 # Node ID 1046a69fabaa55ca9f039efa6d9b6a30d6265553 # Parent f5896dea6fceff30c05a65db63e12c084eb1d5cb dismantle special treatment of citations in Isabelle/Scala; diff -r f5896dea6fce -r 1046a69fabaa src/Pure/PIDE/editor.scala --- 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] = diff -r f5896dea6fce -r 1046a69fabaa src/Pure/PIDE/rendering.scala --- 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 */ diff -r f5896dea6fce -r 1046a69fabaa src/Pure/Thy/bibtex.ML --- 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; diff -r f5896dea6fce -r 1046a69fabaa src/Pure/Thy/bibtex.scala --- 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 **/ diff -r f5896dea6fce -r 1046a69fabaa src/Pure/Thy/sessions.scala --- 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(", ", ", ")") } diff -r f5896dea6fce -r 1046a69fabaa src/Tools/Haskell/Haskell.thy --- 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 = \Markup.citationN\ -citation :: Bytes -> T -citation = markup_string nameN citationN - - {- external resources -} pathN :: Bytes diff -r f5896dea6fce -r 1046a69fabaa src/Tools/VSCode/src/vscode_rendering.scala --- 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 } } diff -r f5896dea6fce -r 1046a69fabaa src/Tools/jEdit/src/completion_popup.scala --- 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 { diff -r f5896dea6fce -r 1046a69fabaa src/Tools/jEdit/src/jedit_rendering.scala --- 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 } }