src/Tools/jEdit/src/symbols_dockable.scala
changeset 56552 76cf86240cb7
parent 55825 694833e3e4a0
child 56599 c4424d8c890f
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Apr 12 21:00:04 2014 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Apr 12 21:38:38 2014 +0200
@@ -85,7 +85,7 @@
         }
       reactions += { case ValueChanged(`search`) => delay_search.invoke() }
     }, "Search Symbols")
-    pages map (p => p.title = (space_explode('_', p.title) map Library.capitalize).mkString(" ") )
+    pages.map(p => p.title = space_explode('_', p.title).map(Library.capitalize(_)).mkString(" "))
   }
   set_content(group_tabs)
 }