src/Pure/PIDE/command.scala

       require(!cmds2.exists(_.is_undefined))
       cmds1.length == cmds2.length &&
         (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
     }
   }
+
+
+  /* resolve inlined files */
+
+  private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
+  {
+    def clean(toks: List[(Token, Int)]): List[(Token, Int)] =
+      toks match {
+        case (t1, i1) :: (t2, i2) :: rest =>
+          if (t1.is_keyword && (t1.source == "%" || t1.source == "--")) clean(rest)
+          else (t1, i1) :: clean((t2, i2) :: rest)
+        case _ => toks
+      }
+    clean(tokens.zipWithIndex.filter({ case (t, _) => t.is_proper }))
+  }
+
+  private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
+    tokens match {
+      case (tok, _) :: toks =>
+        if (tok.is_command)
+          toks.collectFirst({ case (t, i) if t.is_name => (t.content, i) })
+        else None
+      case Nil => None
+    }
+
+  def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
+    span.kind match {
+      case Command_Span.Command_Span(name, _) =>
+        syntax.load_command(name) match {
+          case Some(exts) =>
+            find_file(clean_tokens(span.content)) match {
+              case Some((file, i)) =>
+                if (exts.isEmpty) (List(file), i)
+                else (exts.map(ext => file + "." + ext), i)
+              case None => (Nil, -1)
+            }
+          case None => (Nil, -1)
+        }
+      case _ => (Nil, -1)
+    }
+
+  def resolve_files(
+      resources: Resources,
+      syntax: Prover.Syntax,
+      node_name: Document.Node.Name,
+      span: Command_Span.Span,
+      get_blob: Document.Node.Name => Option[Document.Blob])
+    : (List[Command.Blob], Int) =
+  {
+    val (files, index) = span_files(syntax, span)
+    val blobs =
+      files.map(file =>
+        Exn.capture {
+          val name =
+            Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
+          val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
+          (name, blob)
+        })
+    (blobs, index)
+  }
 }
 
 
 final class Command private(
     val id: Document_ID.Command,