# HG changeset patch
# User wenzelm
# Date 1393243833 -3600
# Node ID ed1b789d0b213668571a8f816c80027727980490
# Parent  734ac5709fbe70f0e0ec78fc55df1c121c4776dc
clarified ML language flags;

diff -r 734ac5709fbe -r ed1b789d0b21 src/Pure/General/completion.scala
--- 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)