tuned;
authorwenzelm
Tue, 25 Feb 2014 18:07:35 +0100
changeset 55746 97f390fa0f3a
parent 55745 b865c3035d5c
child 55747 bef19c929ba5
tuned;
src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Tue Feb 25 17:23:20 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Tue Feb 25 18:07:35 2014 +0100
@@ -290,11 +290,11 @@
   def completion_context(range: Text.Range): Option[Completion.Context] =
     snapshot.select(range, Rendering.completion_context_elements, _ =>
       {
+        case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
+          Some(Completion.Context(language, symbols, antiquotes))
         case Text.Info(_, elem)
         if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
           Some(Completion.Context.ML_inner)
-        case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
-          Some(Completion.Context(language, symbols, antiquotes))
         case Text.Info(_, _) =>
           Some(Completion.Context.inner)
       }).headOption.map(_.info)