tuned;
authorwenzelm
Tue Feb 25 18:07:35 2014 +0100 (2014-02-25 ago)
changeset 5574697f390fa0f3a
parent 55745 b865c3035d5c
child 55747 bef19c929ba5
tuned;
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Feb 25 17:23:20 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Feb 25 18:07:35 2014 +0100
     1.3 @@ -290,11 +290,11 @@
     1.4    def completion_context(range: Text.Range): Option[Completion.Context] =
     1.5      snapshot.select(range, Rendering.completion_context_elements, _ =>
     1.6        {
     1.7 +        case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
     1.8 +          Some(Completion.Context(language, symbols, antiquotes))
     1.9          case Text.Info(_, elem)
    1.10          if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
    1.11            Some(Completion.Context.ML_inner)
    1.12 -        case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
    1.13 -          Some(Completion.Context(language, symbols, antiquotes))
    1.14          case Text.Info(_, _) =>
    1.15            Some(Completion.Context.inner)
    1.16        }).headOption.map(_.info)