--- a/src/Pure/PIDE/command.scala Thu Jan 05 16:44:15 2023 +0100
+++ b/src/Pure/PIDE/command.scala Thu Jan 05 17:00:22 2023 +0100
@@ -26,6 +26,9 @@
object Blobs_Info {
val none: Blobs_Info = Blobs_Info(Nil)
+ def make(blobs: List[(Blob, Document.Blobs.Item)]): Blobs_Info =
+ if (blobs.isEmpty) none else Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a))
+
def errors(msgs: List[String]): Blobs_Info =
Blobs_Info(msgs.map(msg => Exn.Exn[Blob](ERROR(msg))))
}
--- a/src/Pure/PIDE/document.scala Thu Jan 05 16:44:15 2023 +0100
+++ b/src/Pure/PIDE/document.scala Thu Jan 05 17:00:22 2023 +0100
@@ -48,6 +48,10 @@
def apply(blobs: Map[Node.Name, Item]): Blobs = new Blobs(blobs)
val empty: Blobs = apply(Map.empty)
+
+ def make(blobs: List[(Command.Blob, Item)]): Blobs =
+ if (blobs.isEmpty) empty
+ else apply((for ((a, b) <- blobs.iterator) yield a.name -> b).toMap)
}
final class Blobs private(blobs: Map[Node.Name, Blobs.Item]) {
--- a/src/Pure/Tools/build_job.scala Thu Jan 05 16:44:15 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Thu Jan 05 17:00:22 2023 +0100
@@ -71,10 +71,10 @@
val command =
Command.unparsed(thy_source, theory = true, id = id,
node_name = Document.Node.Name(thy_file, theory = theory_context.theory),
- blobs_info = Command.Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a)),
+ blobs_info = Command.Blobs_Info.make(blobs),
markups = markups, results = results)
- val doc_blobs = Document.Blobs((for ((a, b) <- blobs.iterator) yield a.name -> b).toMap)
+ val doc_blobs = Document.Blobs.make(blobs)
Document.State.init.snippet(command, doc_blobs)
}
@@ -298,16 +298,10 @@
override val cache: Term.Cache = store.cache
override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info =
- session_blobs(node_name) match {
- case Nil => Command.Blobs_Info.none
- case blobs => Command.Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a))
- }
+ Command.Blobs_Info.make(session_blobs(node_name))
override def build_blobs(node_name: Document.Node.Name): Document.Blobs =
- session_blobs(node_name) match {
- case Nil => Document.Blobs.empty
- case blobs => Document.Blobs((for ((a, b) <- blobs.iterator) yield a.name -> b).toMap)
- }
+ Document.Blobs.make(session_blobs(node_name))
}
object Build_Session_Errors {