# HG changeset patch
# User wenzelm
# Date 1673626499 -3600
# Node ID 922df6aa16072251e86b78d0bb65ea5a1a4b0d6d
# Parent  c044306db39fcdd8c204db5f047a5a506576f547
clarified signature: more explicit types;

diff -r c044306db39f -r 922df6aa1607 src/Pure/General/completion.scala
--- 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) {
diff -r c044306db39f -r 922df6aa1607 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Jan 13 15:57:11 2023 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Jan 13 17:14:59 2023 +0100
@@ -193,24 +193,21 @@
     val PATH = "path"
     val UNKNOWN = "unknown"
 
-    def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
+    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 unapply(markup: Markup): Option[Value] =
       markup match {
         case Markup(LANGUAGE, props) =>
           (props, props, props, props) match {
             case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
-              Some((name, symbols, antiquotes, delimited))
+              Some(Value(name, symbols, antiquotes, delimited))
             case _ => None
           }
         case _ => None
       }
-
-    object Path {
-      def unapply(markup: Markup): Option[Boolean] =
-        markup match {
-          case Language(PATH, _, _, delimited) => Some(delimited)
-          case _ => None
-        }
-    }
   }
 
 
diff -r c044306db39f -r 922df6aa1607 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Fri Jan 13 15:57:11 2023 +0100
+++ b/src/Pure/PIDE/rendering.scala	Fri Jan 13 17:14:59 2023 +0100
@@ -311,9 +311,8 @@
   def language_context(range: Text.Range): Option[Completion.Language_Context] =
     snapshot.select(range, Rendering.language_context_elements, _ =>
       {
-        case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) =>
-          if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
-          else None
+        case Text.Info(_, XML.Elem(Markup.Language(lang), _)) =>
+          if (lang.delimited) Some(Completion.Language_Context(lang)) else None
         case Text.Info(_, elem)
         if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
           Some(Completion.Language_Context.ML_inner)
@@ -335,8 +334,8 @@
   def language_path(range: Text.Range): Option[Text.Info[Boolean]] =
     snapshot.select(range, Rendering.language_elements, _ =>
       {
-        case Text.Info(info_range, XML.Elem(Markup.Language.Path(delimited), _)) =>
-          Some((delimited, snapshot.convert(info_range)))
+        case Text.Info(info_range, XML.Elem(Markup.Language(lang), _)) if lang.is_path =>
+          Some((lang.delimited, snapshot.convert(info_range)))
         case _ => None
       }).headOption.map({ case Text.Info(_, (delimited, range)) => Text.Info(range, delimited) })
 
@@ -672,9 +671,8 @@
                 if (session.debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
                 else "breakpoint (disabled)"
               Some(info + (r0, true, XML.Text(text)))
-          case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) =>
-            val lang = Word.implode(Word.explode('_', language))
-            Some(info + (r0, true, XML.Text("language: " + lang)))
+          case (info, Text.Info(r0, XML.Elem(Markup.Language(lang), _))) =>
+            Some(info + (r0, true, XML.Text("language: " + lang.description)))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
             val descr = if (kind == "") "expression" else "expression: " + kind
diff -r c044306db39f -r 922df6aa1607 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Fri Jan 13 15:57:11 2023 +0100
+++ b/src/Pure/Tools/update.scala	Fri Jan 13 17:14:59 2023 +0100
@@ -66,8 +66,8 @@
       xml flatMap {
         case XML.Wrapped_Elem(markup, body1, body2) =>
           if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2)
-        case XML.Elem(Markup.Language.Path(_), body)
-        if path_cartouches =>
+        case XML.Elem(Markup.Language(lang), body)
+        if lang.is_path && path_cartouches =>
           Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match {
             case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content)))
             case None => update_xml(body)