# HG changeset patch # User wenzelm # Date 1672747080 -3600 # Node ID cccd1a583c8180a35c34340853ba0ff08f138e3e # Parent 713eb7f2230ef46127834fd8a114a96ea36244f5 clarified modules; diff -r 713eb7f2230e -r cccd1a583c81 src/Pure/PIDE/command.scala --- 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) - } } diff -r 713eb7f2230e -r cccd1a583c81 src/Pure/Tools/build_job.scala --- 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 } }