# 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))