# HG changeset patch
# User wenzelm
# Date 1451643534 -3600
# Node ID e3e22a5e85f2269054c26f70e32ecad671a3f1c2
# Parent  19605292757e9168c20118f29c07eaafe8975569
clarified meaning of \<^bold> action, depending on group;

diff -r 19605292757e -r e3e22a5e85f2 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Fri Jan 01 11:12:43 2016 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Fri Jan 01 11:18:54 2016 +0100
@@ -17,7 +17,7 @@
 
 class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  private class Symbol_Component(val symbol: String) extends Button
+  private class Symbol_Component(val symbol: String, control: Boolean) extends Button
   {
     private val decoded = Symbol.decode(symbol)
     private val font_size = Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
@@ -30,7 +30,7 @@
     action =
       Action(decoded) {
         val text_area = view.getTextArea
-        if (HTML.control_decoded.isDefinedAt(decoded))
+        if (control && HTML.control_decoded.isDefinedAt(decoded))
           Token_Markup.edit_control_style(text_area, decoded)
         else text_area.setSelectedText(decoded)
         text_area.requestFocus
@@ -55,8 +55,9 @@
       Symbol.groups.map({ case (group, symbols) =>
         new TabbedPane.Page(group,
           new ScrollPane(new Wrap_Panel {
-            contents ++= symbols.map(new Symbol_Component(_))
-            if (group == "control") contents += new Reset_Component
+            val control = group == "control"
+            contents ++= symbols.map(new Symbol_Component(_, control))
+            if (control) contents += new Reset_Component
           }), null)
       })
 
@@ -78,7 +79,7 @@
 
             results_panel.contents.clear
             for (sym <- results.take(search_limit))
-              results_panel.contents += new Symbol_Component(sym)
+              results_panel.contents += new Symbol_Component(sym, false)
             if (results.length > search_limit)
               results_panel.contents +=
                 new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }