diff -r c044306db39f -r 922df6aa1607 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Fri Jan 13 15:57:11 2023 +0100
+++ b/src/Pure/General/completion.scala	Fri Jan 13 17:14:59 2023 +0100
@@ -230,6 +230,9 @@
     val ML_outer = Language_Context(Markup.Language.ML, false, true)
     val ML_inner = Language_Context(Markup.Language.ML, true, false)
     val SML_outer = Language_Context(Markup.Language.SML, false, false)
+
+    def apply(lang: Markup.Language.Value): Language_Context =
+      Language_Context(lang.name, lang.symbols, lang.antiquotes)
   }
 
   sealed case class Language_Context(language: String, symbols: Boolean, antiquotes: Boolean) {