proper symbol_length (amending e2e43992f339);
authorwenzelm
Tue, 05 Aug 2025 23:31:30 +0200
changeset 82952 430dcd883bbc
parent 82951 c5b07e7ab7f3
child 82953 d394a77ac023
proper symbol_length (amending e2e43992f339); enforce rebuild of Isabelle/ML;
src/Pure/Build/resources.scala
src/Pure/PIDE/command_span.scala
src/Pure/ROOT.ML
--- 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
         }
--- 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)
--- 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.