--- 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) {