# HG changeset patch
# User wenzelm
# Date 1393166301 -3600
# Node ID 13b58baf994b64ea3d394b372b759395502d7e97
# Parent  767edb2c1e4e5214ffa131e526d4d7a6e6412629
tuned;

diff -r 767edb2c1e4e -r 13b58baf994b src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 15:35:19 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 15:38:21 2014 +0100
@@ -348,12 +348,10 @@
   /* highlighted area */
 
   def highlight(range: Text.Range): Option[Text.Info[Color]] =
-  {
     snapshot.select(range, Rendering.highlight_elements, _ =>
       {
         case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
-      }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
-  }
+      }).headOption.map(_.info)
 
 
   /* hyperlinks */
@@ -430,8 +428,7 @@
             }
           }
           else Some(Text.Info(snapshot.convert(info_range), elem))
-      }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
-
+      }).headOption.map(_.info)
 
   def command_results(range: Text.Range): Command.Results =
   {