# HG changeset patch
# User wenzelm
# Date 1607168601 -3600
# Node ID 1c378ab75d4846b84ede80a368ba31e083e92080
# Parent  ea4f86914cb29cbeff06d2515a35b5d8ef756239
clarified signature, notably access to blob files;

diff -r ea4f86914cb2 -r 1c378ab75d48 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Dec 05 12:14:40 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Dec 05 12:43:21 2020 +0100
@@ -16,11 +16,23 @@
 {
   /* blobs */
 
+  object Blob
+  {
+    def read_file(name: Document.Node.Name, src_path: Path): Blob =
+    {
+      val bytes = Bytes.read(name.path)
+      val chunk = Symbol.Text_Chunk(bytes.text)
+      Blob(name, src_path, Some((bytes.sha1_digest, chunk)))
+    }
+  }
+
   sealed case class Blob(
     name: Document.Node.Name,
     src_path: Path,
     content: Option[(SHA1.Digest, Symbol.Text_Chunk)])
   {
+    def read_file: String = File.read(name.path)
+
     def chunk_file: Symbol.Text_Chunk.File =
       Symbol.Text_Chunk.File(name.node)
   }
@@ -479,12 +491,10 @@
         file <- span.loaded_files(syntax).files
       } yield {
         (Exn.capture {
-          val dir = Path.explode(node_name.master_dir)
+          val dir = node_name.master_dir_path
           val src_path = Path.explode(file)
           val name = Document.Node.Name((dir + src_path).expand.implode_symbolic)
-          val bytes = Bytes.read(name.path)
-          val chunk = Symbol.Text_Chunk(bytes.text)
-          Blob(name, src_path, Some((bytes.sha1_digest, chunk)))
+          Blob.read_file(name, src_path)
         }).user_error
       }
     Blobs_Info(blobs, -1)
diff -r ea4f86914cb2 -r 1c378ab75d48 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Dec 05 12:14:40 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 05 12:43:21 2020 +0100
@@ -558,6 +558,13 @@
     def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
 
     def get_snippet_command: Option[Command]
+
+    def node_files: List[Node.Name] =
+      get_snippet_command match {
+        case None => List(node_name)
+        case Some(command) => node_name :: command.blobs_names
+      }
+
     def command_snippet(command: Command): Snapshot =
     {
       val node_name = command.node_name
@@ -582,9 +589,19 @@
       range: Text.Range = Text.Range.full,
       elements: Markup.Elements = Markup.Elements.full): XML.Body
 
-    def xml_markup_blobs(
-      read_blob: Node.Name => String,
-      elements: Markup.Elements = Markup.Elements.full): List[(XML.Body, Command.Blob)]
+    def xml_markup_blobs(elements: Markup.Elements = Markup.Elements.full): List[XML.Body] =
+    {
+      get_snippet_command match {
+        case None => Nil
+        case Some(command) =>
+          for (Exn.Res(blob) <- command.blobs)
+          yield {
+            val text = blob.read_file
+            val markup = command.init_markups(Command.Markup_Index.blob(blob))
+            markup.to_XML(Text.Range(0, text.length), text, elements)
+          }
+      }
+    }
 
     def messages: List[(XML.Tree, Position.T)]
     def exports: List[Export.Entry]
@@ -1161,22 +1178,6 @@
             elements: Markup.Elements = Markup.Elements.full): XML.Body =
           state.xml_markup(version, node_name, range = range, elements = elements)
 
-        def xml_markup_blobs(read_blob: Node.Name => String,
-          elements: Markup.Elements = Markup.Elements.full): List[(XML.Body, Command.Blob)] =
-        {
-          get_snippet_command match {
-            case None => Nil
-            case Some(command) =>
-              for (Exn.Res(blob) <- command.blobs)
-              yield {
-                val text = read_blob(blob.name)
-                val markup = command.init_markups(Command.Markup_Index.blob(blob))
-                val xml = markup.to_XML(Text.Range(0, text.size), text, elements)
-                (xml, blob)
-              }
-          }
-        }
-
         lazy val messages: List[(XML.Tree, Position.T)] =
           (for {
             (command, start) <-
diff -r ea4f86914cb2 -r 1c378ab75d48 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Dec 05 12:14:40 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Dec 05 12:43:21 2020 +0100
@@ -124,7 +124,7 @@
   def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name, spans: List[Command_Span.Span])
     : List[Path] =
   {
-    val dir = Path.explode(name.master_dir)
+    val dir = name.master_dir_path
     for { span <- spans; file <- span.loaded_files(syntax).files }
       yield (dir + Path.explode(file)).expand
   }
diff -r ea4f86914cb2 -r 1c378ab75d48 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Dec 05 12:14:40 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Dec 05 12:43:21 2020 +0100
@@ -187,13 +187,12 @@
             def export_text(name: String, text: String): Unit =
               export(name, List(XML.Text(text)))
 
-            val blobs = snapshot.xml_markup_blobs(name => File.read(name.path))
-            val chunks = for ((_, blob) <- blobs) yield blob.name.symbolic.node
-            export_text(Export.FILES, cat_lines(snapshot.node_name.symbolic.node :: chunks))
+            export_text(Export.FILES, cat_lines(snapshot.node_files.map(_.symbolic.node)))
 
-            for (((xml, _), i) <- blobs.zipWithIndex) export(Export.MARKUP + (i + 1), xml)
+            for ((xml, i) <- snapshot.xml_markup_blobs().zipWithIndex) {
+              export(Export.MARKUP + (i + 1), xml)
+            }
             export(Export.MARKUP, snapshot.xml_markup())
-
             export(Export.MESSAGES, snapshot.messages.map(_._1))
 
             val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info))