changeset 76967 | 38e19412cf31 |
parent 76965 | 922df6aa1607 |
child 77368 | 7c57d9586f4c |
--- 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) }