# HG changeset patch
# User wenzelm
# Date 1646319902 -3600
# Node ID 1ced8ee860e2619e8f381e19abdd069df3bdd97b
# Parent  19f1d8c074c86393d2b9e0fe9734bc7b6b251471
clarified signature;

diff -r 19f1d8c074c8 -r 1ced8ee860e2 src/Pure/General/completion.scala
--- 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 = "@{"
 
diff -r 19f1d8c074c8 -r 1ced8ee860e2 src/Pure/General/symbol.scala
--- 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 */
diff -r 19f1d8c074c8 -r 1ced8ee860e2 src/Tools/VSCode/src/lsp.scala
--- 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,
diff -r 19f1d8c074c8 -r 1ced8ee860e2 src/Tools/jEdit/src/symbols_dockable.scala
--- 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