src/Tools/jEdit/src/rendering.scala
changeset 55616 25a7a998852a
parent 55615 bf4bbe72f740
child 55619 c5aeeacdd2b1
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 12:53:12 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 13:23:49 2014 +0100
     1.3 @@ -206,7 +206,7 @@
     1.4      Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE,
     1.5        Markup.COMMENT, Markup.LANGUAGE)
     1.6  
     1.7 -  def completion_context(caret: Text.Offset): Completion.Context =
     1.8 +  def completion_context(caret: Text.Offset): Option[Completion.Context] =
     1.9      if (caret > 0) {
    1.10        val result =
    1.11          snapshot.select_markup(Text.Range(caret - 1, caret + 1), Some(completion_elements), _ =>
    1.12 @@ -214,15 +214,16 @@
    1.13              case Text.Info(_, XML.Elem(Markup.Language(language, symbols), _)) =>
    1.14                Some(Completion.Context(language, symbols))
    1.15              case Text.Info(_, XML.Elem(markup, _)) =>
    1.16 -              if (completion_elements(markup.name)) Some(Completion.Context("unknown", true))
    1.17 +              if (completion_elements(markup.name))
    1.18 +                Some(Completion.Context(Markup.Language.UNKNOWN, true))
    1.19                else None
    1.20            })
    1.21        result match {
    1.22 -        case Text.Info(_, context) :: _ => context
    1.23 -        case Nil => Completion.Context.default
    1.24 +        case Text.Info(_, context) :: _ => Some(context)
    1.25 +        case Nil => None
    1.26        }
    1.27      }
    1.28 -    else Completion.Context.default
    1.29 +    else None
    1.30  
    1.31  
    1.32    /* command overview */