src/Tools/jEdit/src/rendering.scala
changeset 55687 78c83cd477c1
parent 55674 8a213ab0e78a
child 55688 767edb2c1e4e
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 10:44:57 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Feb 23 14:39:51 2014 +0100
     1.3 @@ -150,7 +150,7 @@
     1.4  
     1.5    /* markup elements */
     1.6  
     1.7 -  private val completion_reported_elements = Set(Markup.COMPLETION)
     1.8 +  private val completion_names_elements = Set(Markup.COMPLETION)
     1.9  
    1.10    private val completion_context_elements =
    1.11      Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    1.12 @@ -273,20 +273,17 @@
    1.13  
    1.14    /* completion */
    1.15  
    1.16 -  def completion_reported(caret: Text.Offset): Option[Completion.Reported] =
    1.17 -    if (caret > 0)
    1.18 +  def completion_names(caret: Text.Offset): Option[Completion.Names] =
    1.19 +    if (caret > 0 && !snapshot.is_outdated)
    1.20      {
    1.21        val result =
    1.22          snapshot.select(Text.Range(caret - 1, caret + 1),
    1.23 -          Rendering.completion_reported_elements, _ =>
    1.24 +          Rendering.completion_names_elements, _ =>
    1.25            {
    1.26 -            case Text.Info(_, Completion.Reported.Elem(reported)) => Some(reported)
    1.27 +            case Completion.Names.Info(names) => Some(names)
    1.28              case _ => None
    1.29            })
    1.30 -      result match {
    1.31 -        case Text.Info(_, reported) :: _ => Some(reported)
    1.32 -        case Nil => None
    1.33 -      }
    1.34 +      result.headOption.map(_.info)
    1.35      }
    1.36      else None
    1.37  
    1.38 @@ -304,10 +301,7 @@
    1.39              case Text.Info(_, _) =>
    1.40                Some(Completion.Context.inner)
    1.41            })
    1.42 -      result match {
    1.43 -        case Text.Info(_, context) :: _ => Some(context)
    1.44 -        case Nil => None
    1.45 -      }
    1.46 +      result.headOption.map(_.info)
    1.47      }
    1.48      else None
    1.49