diff -r 2f91b787f509 -r 38e19412cf31 src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Fri Jan 13 19:07:18 2023 +0100 +++ b/src/Pure/General/completion.scala Fri Jan 13 19:16:24 2023 +0100 @@ -231,7 +231,7 @@ 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 = + def apply(lang: Markup.Language): Language_Context = Language_Context(lang.name, lang.symbols, lang.antiquotes) }