# HG changeset patch
# User wenzelm
# Date 1753627285 -7200
# Node ID f7db39778e549d09a798209bcc4fc5f31a9b0c24
# Parent  a27841dcd7df44d38714ee40394f58d057ab8926
clarified signature;

diff -r a27841dcd7df -r f7db39778e54 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Jul 27 16:28:10 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Jul 27 16:41:25 2025 +0200
@@ -816,11 +816,11 @@
 
     /* command spans --- according to PIDE markup */
 
-    def command_spans(range: Text.Range): List[Text.Info[Markup.Command_Span.Arg]] =
+    def command_spans(range: Text.Range): List[Text.Info[Markup.Command_Span.Args]] =
       select(range, Markup.Elements(Markup.COMMAND_SPAN), _ =>
         {
-          case Text.Info(range, XML.Elem(Markup.Command_Span(arg), _)) =>
-            Some(Text.Info(range, arg))
+          case Text.Info(range, XML.Elem(Markup.Command_Span(args), _)) =>
+            Some(Text.Info(range, args))
           case _ => None
         }).map(_.info)
   }
diff -r a27841dcd7df -r f7db39778e54 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Jul 27 16:28:10 2025 +0200
+++ b/src/Pure/PIDE/markup.scala	Sun Jul 27 16:41:25 2025 +0200
@@ -445,21 +445,21 @@
   object Command_Span {
     val Is_Begin = new Properties.Boolean("is_begin")
 
-    sealed case class Arg(name: String, kind: String, is_begin: Boolean) {
+    sealed case class Args(name: String, kind: String, is_begin: Boolean) {
       def properties: Properties.T =
         (if (name.isEmpty) Nil else Name(name)) :::
         (if (kind.isEmpty) Nil else Kind(kind)) :::
         (if (!is_begin) Nil else Is_Begin(is_begin))
     }
 
-    def apply(arg: Arg): Markup = Markup(COMMAND_SPAN, arg.properties)
+    def apply(args: Args): Markup = Markup(COMMAND_SPAN, args.properties)
     def apply(name: String, kind: String, is_begin: Boolean): Markup =
-      apply(Arg(name, kind, is_begin))
+      apply(Args(name, kind, is_begin))
 
-    def unapply(markup: Markup): Option[Arg] =
+    def unapply(markup: Markup): Option[Args] =
       if (markup.name == COMMAND_SPAN) {
         val props = markup.properties
-        Some(Arg(Name.get(props), Kind.get(props), Is_Begin.get(props)))
+        Some(Args(Name.get(props), Kind.get(props), Is_Begin.get(props)))
       }
       else None
   }