# HG changeset patch
# User wenzelm
# Date 1607191779 -3600
# Node ID 1975f397eabbf8ee57f7faac658192bc3a10f7f8
# Parent  fa5d8f48638014430713ff691372d948d503910f
proper span position for blobs in batch-build (but: practically irrelevant);

diff -r fa5d8f486380 -r 1975f397eabb src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Dec 05 18:14:55 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Dec 05 19:09:39 2020 +0100
@@ -594,7 +594,7 @@
           val opt_range =
             reported_range orElse {
               if (name == Symbol.Text_Chunk.Default)
-                Position.Range.unapply(span.position)
+                Position.Range.unapply(span.absolute_position)
               else None
             }
           opt_range match {