# HG changeset patch
# User wenzelm
# Date 1673020456 -3600
# Node ID da3310cc00f042dc61de24f140db23f02a216ea7
# Parent  fffb978dd683a25516aff8db1a74b4059d0b3bcf
tuned signature: avoid alias that is unclear wrt. lazy state and Symbol.encode/decode status;

diff -r fffb978dd683 -r da3310cc00f0 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Jan 06 16:50:43 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Jan 06 16:54:16 2023 +0100
@@ -67,7 +67,6 @@
     override def toString: String = name
 
     def bytes: Bytes = if (compressed) body.uncompress(cache = cache) else body
-    def text: String = bytes.text
   }
 
   object Sources {
diff -r fffb978dd683 -r da3310cc00f0 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Jan 06 16:50:43 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Fri Jan 06 16:54:16 2023 +0100
@@ -51,7 +51,7 @@
             Document.Blobs.Item(bytes, text, chunk, changed = false)
         }
 
-      val thy_source = read_source_file(thy_file).text
+      val thy_source = read_source_file(thy_file).bytes.text
       val thy_xml = read_xml(Export.MARKUP)
       val blobs_xml =
         for (i <- (1 to blobs.length).toList)