# HG changeset patch
# User wenzelm
# Date 1754429490 -7200
# Node ID 430dcd883bbc5002446ebe5df9b33b65a57f82d2
# Parent  c5b07e7ab7f312d93c9d25d0822c2420adca5fb2
proper symbol_length (amending e2e43992f339);
enforce rebuild of Isabelle/ML;

diff -r c5b07e7ab7f3 -r 430dcd883bbc src/Pure/Build/resources.scala
--- a/src/Pure/Build/resources.scala	Tue Aug 05 22:24:29 2025 +0200
+++ b/src/Pure/Build/resources.scala	Tue Aug 05 23:31:30 2025 +0200
@@ -100,7 +100,7 @@
           var offset = 1
           for (span <- spans) {
             if (span.is_load_command(syntax)) { result += (span -> offset) }
-            offset += span.length
+            offset += span.symbol_length
           }
           result.toList
         }
diff -r c5b07e7ab7f3 -r 430dcd883bbc src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Tue Aug 05 22:24:29 2025 +0200
+++ b/src/Pure/PIDE/command_span.scala	Tue Aug 05 23:31:30 2025 +0200
@@ -102,6 +102,7 @@
     def content_reader: CharSequenceReader = Scan.char_reader(Token.implode(content))
 
     def length: Int = content.foldLeft(0)(_ + _.source.length)
+    def symbol_length: Symbol.Offset = content.foldLeft(0)(_ + _.symbol_length)
 
     def compact_source: (String, Span) = {
       val source = Token.implode(content)
diff -r c5b07e7ab7f3 -r 430dcd883bbc src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Aug 05 22:24:29 2025 +0200
+++ b/src/Pure/ROOT.ML	Tue Aug 05 23:31:30 2025 +0200
@@ -1,6 +1,6 @@
 (*  Title:      Pure/ROOT.ML
     Author:     Makarius
-    UUID:       65c4f1c9-5db7-4528-b719-40dbb49a0791
+    UUID:       2dddcab9-800b-4158-b53a-f20f73aa7663
 
 Main entry point for the Isabelle/Pure bootstrap process.