src/Tools/jEdit/src/rendering.scala
changeset 55689 13b58baf994b
parent 55688 767edb2c1e4e
child 55690 d73949233c2e
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 15:35:19 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 15:38:21 2014 +0100
     1.3 @@ -348,12 +348,10 @@
     1.4    /* highlighted area */
     1.5  
     1.6    def highlight(range: Text.Range): Option[Text.Info[Color]] =
     1.7 -  {
     1.8      snapshot.select(range, Rendering.highlight_elements, _ =>
     1.9        {
    1.10          case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
    1.11 -      }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
    1.12 -  }
    1.13 +      }).headOption.map(_.info)
    1.14  
    1.15  
    1.16    /* hyperlinks */
    1.17 @@ -430,8 +428,7 @@
    1.18              }
    1.19            }
    1.20            else Some(Text.Info(snapshot.convert(info_range), elem))
    1.21 -      }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
    1.22 -
    1.23 +      }).headOption.map(_.info)
    1.24  
    1.25    def command_results(range: Text.Range): Command.Results =
    1.26    {