--- a/src/Pure/PIDE/command.scala Mon Jan 02 20:39:21 2023 +0100
+++ b/src/Pure/PIDE/command.scala Tue Jan 03 12:58:00 2023 +0100
@@ -471,26 +471,6 @@
Blobs_Info(blobs, index = loaded_files.index)
}
}
-
- def build_blobs_info(
- syntax: Outer_Syntax,
- node_name: Document.Node.Name,
- load_commands: List[Command_Span.Span]
- ): Blobs_Info = {
- val blobs =
- for {
- span <- load_commands
- file <- span.loaded_files(syntax).files
- } yield {
- (Exn.capture {
- val dir = node_name.master_dir_path
- val src_path = Path.explode(file)
- val name = Document.Node.Name((dir + src_path).expand.implode_symbolic)
- Blob.read_file(name, src_path)
- }).user_error
- }
- Blobs_Info(blobs)
- }
}
--- a/src/Pure/Tools/build_job.scala Mon Jan 02 20:39:21 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Tue Jan 03 12:58:00 2023 +0100
@@ -275,11 +275,21 @@
new Session(options, resources) {
override val cache: Term.Cache = store.cache
- override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = {
- session_background.base.theory_load_commands.get(name.theory) match {
+ override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info = {
+ session_background.base.theory_load_commands.get(node_name.theory) match {
case Some(spans) =>
- val syntax = session_background.base.theory_syntax(name)
- Command.build_blobs_info(syntax, name, spans)
+ val syntax = session_background.base.theory_syntax(node_name)
+ val blobs =
+ for (span <- spans; file <- span.loaded_files(syntax).files)
+ yield {
+ (Exn.capture {
+ val dir = node_name.master_dir_path
+ val src_path = Path.explode(file)
+ val name = Document.Node.Name((dir + src_path).expand.implode_symbolic)
+ Command.Blob.read_file(name, src_path)
+ }).user_error
+ }
+ Command.Blobs_Info(blobs)
case None => Command.Blobs_Info.none
}
}