src/Tools/jEdit/src/symbols_dockable.scala

--- a/src/Tools/jEdit/src/symbols_dockable.scala	Fri Aug 30 11:00:46 2013 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Fri Aug 30 11:04:29 2013 +0200
@@ -43,8 +43,7 @@
       }
     tooltip =
       JEdit_Lib.wrap_tooltip(
-        symbol +
-          (if (Symbol.abbrevs.isDefinedAt(symbol)) "\nabbrev: " + Symbol.abbrevs(symbol) else ""))
+        cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a)))
   }
 
   private class Reset_Component extends Button