src/Pure/General/completion.scala
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)
   }