src/Pure/PIDE/command.scala

   /* make commands */
 
   def name(span: List[Token]): String =
     span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
 
+  type Blobs = List[(Document.Node.Name, Option[SHA1.Digest])]
+
   def apply(
     id: Document_ID.Command,
     node_name: Document.Node.Name,
     span: List[Token],
-    thy_load: Option[List[String]],
+    blobs: Blobs,
     results: Results = Results.empty,
     markup: Markup_Tree = Markup_Tree.empty): Command =
   {
     val source: String =
       span match {

       val s1 = source.substring(i, i + n)
       span1 += Token(kind, s1)
       i += n
     }
 
-    new Command(id, node_name, span1.toList, source, thy_load, results, markup)
-  }
-
-  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, None)
+    new Command(id, node_name, span1.toList, source, blobs, results, markup)
+  }
+
+  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
 
   def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
       : Command =
-    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), None,
+    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), Nil,
       results, markup)
 
   def unparsed(source: String): Command =
     unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
 

 final class Command private(
     val id: Document_ID.Command,
     val node_name: Document.Node.Name,
     val span: List[Token],
     val source: String,
-    val thy_load: Option[List[String]],
+    val blobs: Command.Blobs,
     val init_results: Command.Results,
     val init_markup: Markup_Tree)
 {
   /* classification */