src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Mon Sep 22 14:01:37 2025 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon Sep 22 15:55:47 2025 +0200
@@ -708,6 +708,7 @@
       }
   }
 
+  val Command_Offset = new Properties.Int("command_offset")
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
   def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)