src/Pure/PIDE/rendering.scala
changeset 76965 922df6aa1607
parent 76858 39db5e268aaf
child 77029 1046a69fabaa
--- 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