--- a/src/Pure/General/completion.scala Thu Mar 03 15:47:54 2022 +0100
+++ b/src/Pure/General/completion.scala Thu Mar 03 16:05:02 2022 +0100
@@ -320,7 +320,8 @@
/* abbreviations */
private def symbol_abbrevs: Thy_Header.Abbrevs =
- for ((sym, abbr) <- Symbol.symbols.abbrevs.toList) yield (abbr, sym)
+ for (entry <- Symbol.symbols.entries; abbrev <- entry.abbrevs)
+ yield (abbrev, entry.symbol)
private val antiquote = "@{"
--- a/src/Pure/General/symbol.scala Thu Mar 03 15:47:54 2022 +0100
+++ b/src/Pure/General/symbol.scala Thu Mar 03 16:05:02 2022 +0100
@@ -439,8 +439,8 @@
} yield entry.symbol -> group)
.toList.groupBy(_._2).toList.map({ case (g, list) => (g, list.map(_._1)) }).sortBy(_._1)
- val abbrevs: Multi_Map[Symbol, String] =
- Multi_Map.from(for (entry <- entries; a <- entry.abbrevs.reverse) yield entry.symbol -> a)
+ def get_abbrevs(sym: Symbol): List[String] =
+ get(sym) match { case Some(entry) => entry.abbrevs case _ => Nil }
/* recoding */
--- a/src/Tools/VSCode/src/lsp.scala Thu Mar 03 15:47:54 2022 +0100
+++ b/src/Tools/VSCode/src/lsp.scala Thu Mar 03 16:05:02 2022 +0100
@@ -161,7 +161,7 @@
"completionProvider" -> JSON.Object(
"resolveProvider" -> false,
"triggerCharacters" ->
- Symbol.symbols.abbrevs.values.flatMap(_.iterator).map(_.toString).toList.distinct
+ Symbol.symbols.entries.flatMap(_.abbrevs).flatMap(_.toList).map(_.toString).distinct
),
"hoverProvider" -> true,
"definitionProvider" -> true,
--- a/src/Tools/jEdit/src/symbols_dockable.scala Thu Mar 03 15:47:54 2022 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Thu Mar 03 16:05:02 2022 +0100
@@ -104,7 +104,7 @@
}
tooltip =
GUI.tooltip_lines(
- cat_lines(symbol :: Symbol.symbols.abbrevs.get_list(symbol).map(a => "abbrev: " + a)))
+ cat_lines(symbol :: Symbol.symbols.get_abbrevs(symbol).map(a => "abbrev: " + a)))
}
private class Reset_Component extends Button