# HG changeset patch
# User wenzelm
# Date 1673633784 -3600
# Node ID 38e19412cf310f4d0359ad5e7a54d8a72970dbd1
# Parent  2f91b787f509897bed5f6a40912fac142139dd37
clarified types;

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)
   }
 
diff -r 2f91b787f509 -r 38e19412cf31 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Jan 13 19:07:18 2023 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Jan 13 19:16:24 2023 +0100
@@ -193,24 +193,33 @@
     val PATH = "path"
     val UNKNOWN = "unknown"
 
-    sealed case class Value(name: String, symbols: Boolean, antiquotes: Boolean, delimited: Boolean) {
-      def is_path: Boolean = name == PATH
-      def description: String = Word.implode(Word.explode('_', name))
-    }
+    def apply(name: String, symbols: Boolean, antiquotes: Boolean, delimited: Boolean): Language =
+      new Language(name, symbols, antiquotes, delimited)
 
-    val outer: Value = Value("", true, false, false)
+    val outer: Language = apply("", true, false, false)
 
-    def unapply(markup: Markup): Option[Value] =
+    def unapply(markup: Markup): Option[Language] =
       markup match {
         case Markup(LANGUAGE, props) =>
           (props, props, props, props) match {
             case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
-              Some(Value(name, symbols, antiquotes, delimited))
+              Some(apply(name, symbols, antiquotes, delimited))
             case _ => None
           }
         case _ => None
       }
   }
+  class Language private(
+    val name: String,
+    val symbols: Boolean,
+    val antiquotes: Boolean,
+    val delimited: Boolean
+  ) {
+    override def toString: String = name
+
+    def is_path: Boolean = name == PATH
+    def description: String = Word.implode(Word.explode('_', name))
+  }
 
 
   /* external resources */
diff -r 2f91b787f509 -r 38e19412cf31 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Fri Jan 13 19:07:18 2023 +0100
+++ b/src/Pure/Tools/update.scala	Fri Jan 13 19:16:24 2023 +0100
@@ -62,7 +62,7 @@
 
     val path_cartouches = options.bool("update_path_cartouches")
 
-    def update_xml(lang: Markup.Language.Value, xml: XML.Body): XML.Body =
+    def update_xml(lang: Markup.Language, xml: XML.Body): XML.Body =
       xml flatMap {
         case XML.Wrapped_Elem(markup, body1, body2) =>
           val body = if (markup.name == Markup.UPDATE) body1 else body2