src/Pure/PIDE/command.scala
changeset 38427 7066fbd315ae
parent 38426 2858ec7b6dd8
child 38429 9951852fae91
     1.1 --- a/src/Pure/PIDE/command.scala	Sun Aug 15 22:48:56 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sun Aug 15 23:07:22 2010 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4  
     1.5      def type_at(pos: Text.Offset): Option[String] =
     1.6      {
     1.7 -      types.find(t => t.range.start <= pos && pos < t.range.stop) match {
     1.8 +      types.find(_.range.contains(pos)) match {
     1.9          case Some(t) =>
    1.10            t.info match {
    1.11              case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
    1.12 @@ -82,7 +82,7 @@
    1.13          case _ => false }).flatten
    1.14  
    1.15      def ref_at(pos: Text.Offset): Option[Markup_Node] =
    1.16 -      refs.find(t => t.range.start <= pos && pos < t.range.stop)
    1.17 +      refs.find(_.range.contains(pos))
    1.18  
    1.19  
    1.20      /* message dispatch */