# HG changeset patch
# User wenzelm
# Date 1515516025 -3600
# Node ID 7e21d19e7ad73b783994b3b4c61bf902d08e11c4
# Parent  5fc0b0c9a735d940bc815d79784f76622f7807ba
show only symbols with code;

diff -r 5fc0b0c9a735 -r 7e21d19e7ad7 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Jan 09 17:09:34 2018 +0100
+++ b/src/Pure/General/symbol.scala	Tue Jan 09 17:40:25 2018 +0100
@@ -514,6 +514,14 @@
   def groups: List[(String, List[Symbol])] = symbols.groups
   def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs
   def codes: List[(Symbol, Int)] = symbols.codes
+  def groups_code: List[(String, List[Symbol])] =
+  {
+    val has_code = codes.iterator.map(_._1).toSet
+    groups.flatMap({ case (group, symbols) =>
+      val symbols1 = symbols.filter(has_code)
+      if (symbols1.isEmpty) None else Some((group, symbols1))
+    })
+  }
 
   lazy val is_code: Int => Boolean = codes.map(_._2).toSet
   def decode(text: String): String = symbols.decode(text)
diff -r 5fc0b0c9a735 -r 7e21d19e7ad7 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Tue Jan 09 17:09:34 2018 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Tue Jan 09 17:40:25 2018 +0100
@@ -127,8 +127,7 @@
     layout(search_field) = BorderPanel.Position.North
     layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
 
-    val search_space =
-      (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
+    val search_space = for ((sym, _) <- Symbol.codes) yield (sym, Word.lowercase(sym))
     val search_delay =
       GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
         val search_words = Word.explode(Word.lowercase(search_field.text))
@@ -155,7 +154,7 @@
     pages += new TabbedPane.Page("abbrevs", abbrevs_panel)
 
     pages ++=
-      Symbol.groups.map({ case (group, symbols) =>
+      Symbol.groups_code.map({ case (group, symbols) =>
         val control = group == "control"
         new TabbedPane.Page(group,
           new ScrollPane(Wrap_Panel(