1.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 23:42:43 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Feb 22 15:07:33 2014 +0100
     1.3 @@ -278,11 +278,11 @@
     1.4            {
     1.5              case Text.Info(_, elem)
     1.6              if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
     1.7 -              Some(Completion.Context(Markup.Language.ML, true))
     1.8 -            case Text.Info(_, XML.Elem(Markup.Language(language, symbols), _)) =>
     1.9 -              Some(Completion.Context(language, symbols))
    1.10 -            case Text.Info(_, XML.Elem(markup, _)) =>
    1.11 -              Some(Completion.Context(Markup.Language.UNKNOWN, true))
    1.12 +              Some(Completion.Context.ML_inner)
    1.13 +            case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
    1.14 +              Some(Completion.Context(language, symbols, antiquotes))
    1.15 +            case Text.Info(_, _) =>
    1.16 +              Some(Completion.Context.inner)
    1.17            })
    1.18        result match {
    1.19          case Text.Info(_, context) :: _ => Some(context)
    1.20 @@ -500,7 +500,7 @@
    1.21              Some(add(prev, r, (true, pretty_typing("::", body))))
    1.22            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
    1.23              Some(add(prev, r, (false, pretty_typing("ML:", body))))
    1.24 -          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _), _))) =>
    1.25 +          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _), _))) =>
    1.26              Some(add(prev, r, (true, XML.Text("language: " + language))))
    1.27            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
    1.28              Rendering.tooltip_descriptions.get(name).