clarified modules;
authorwenzelm
Tue, 03 Jan 2023 12:58:00 +0100
changeset 76879 cccd1a583c81
parent 76873 713eb7f2230e
child 76880 6a07cf09604d
clarified modules;
src/Pure/PIDE/command.scala
src/Pure/Tools/build_job.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)
-  }
 }
 
 
--- 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
             }
           }