clarified ML language flags;
authorwenzelm
Mon, 24 Feb 2014 13:10:33 +0100
changeset 55714 ed1b789d0b21
parent 55713 734ac5709fbe
child 55715 bc04f1ab3c3a
clarified ML language flags;
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)