--- a/src/Pure/General/completion.scala Mon Feb 24 12:51:55 2014 +0100
+++ b/src/Pure/General/completion.scala Mon Feb 24 13:10:33 2014 +0100
@@ -170,8 +170,8 @@
{
val outer = Context("", true, false)
val inner = Context(Markup.Language.UNKNOWN, true, false)
- val ML_outer = Context(Markup.Language.ML, false, false)
- val ML_inner = Context(Markup.Language.ML, true, true)
+ val ML_outer = Context(Markup.Language.ML, false, true)
+ val ML_inner = Context(Markup.Language.ML, true, false)
}
sealed case class Context(language: String, symbols: Boolean, antiquotes: Boolean)