src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Sun Mar 15 14:46:01 2015 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Mar 15 19:21:15 2015 +0100
@@ -15,8 +15,10 @@
 object Command
 {
   type Edit = (Option[Command], Option[Command])
+
   type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Symbol.Text_Chunk)])]
-
+  type Blobs_Info = (List[Blob], Int)
+  val no_blobs: Blobs_Info = (Nil, -1)
 
 
   /** accumulated results from prover **/
@@ -253,17 +255,15 @@
   def apply(
     id: Document_ID.Command,
     node_name: Document.Node.Name,
-    blobs: Option[(List[Blob], Int)],
+    blobs_info: Blobs_Info,
     span: Command_Span.Span): Command =
   {
     val (source, span1) = span.compact_source
-    val (blobs_list, blobs_index) = blobs.getOrElse((Nil, -1))
-    new Command(
-      id, node_name, blobs_list, blobs_index, span1, source, Results.empty, Markup_Tree.empty)
+    new Command(id, node_name, blobs_info, span1, source, Results.empty, Markup_Tree.empty)
   }
 
   val empty: Command =
-    Command(Document_ID.none, Document.Node.Name.empty, None, Command_Span.empty)
+    Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty)
 
   def unparsed(
     id: Document_ID.Command,
@@ -272,7 +272,7 @@
     markup: Markup_Tree): Command =
   {
     val (source1, span1) = Command_Span.unparsed(source).compact_source
-    new Command(id, Document.Node.Name.empty, Nil, -1, span1, source1, results, markup)
+    new Command(id, Document.Node.Name.empty, no_blobs, span1, source1, results, markup)
   }
 
   def unparsed(source: String): Command =
@@ -309,7 +309,7 @@
   }
 
 
-  /* resolve inlined files */
+  /* blobs: inlined errors and auxiliary files */
 
   private def clean_tokens(tokens: List[Token]): List[(Token, Int)] =
   {
@@ -348,23 +348,36 @@
       case _ => (Nil, -1)
     }
 
-  def resolve_files(
+  def blobs_info(
     resources: Resources,
     syntax: Prover.Syntax,
     get_blob: Document.Node.Name => Option[Document.Blob],
+    can_import: Document.Node.Name => Boolean,
     node_name: Document.Node.Name,
-    span: Command_Span.Span): (List[Command.Blob], Int) =
+    header: Document.Node.Header,
+    span: Command_Span.Span): Blobs_Info =
   {
-    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)
-        }).user_error)
-    (blobs, index)
+    span.kind match {
+      // inlined errors
+      case Command_Span.Command_Span(name, _) if syntax.is_theory_begin(name) =>
+        val import_errors =
+          for ((imp, pos) <- header.imports if !can_import(imp))
+            yield "Bad theory import " + quote(imp.node) + Position.here(pos)
+        ((header.errors ::: import_errors).map(msg => Exn.Exn(ERROR(msg)): Command.Blob), -1)
+
+      // auxiliary files
+      case _ =>
+        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)
+            }).user_error)
+        (blobs, index)
+    }
   }
 }
 
@@ -372,8 +385,7 @@
 final class Command private(
     val id: Document_ID.Command,
     val node_name: Document.Node.Name,
-    val blobs: List[Command.Blob],
-    val blobs_index: Int,
+    val blobs_info: Command.Blobs_Info,
     val span: Command_Span.Span,
     val source: String,
     val init_results: Command.Results,
@@ -402,6 +414,9 @@
 
   /* blobs */
 
+  def blobs: List[Command.Blob] = blobs_info._1
+  def blobs_index: Int = blobs_info._2
+
   def blobs_names: List[Document.Node.Name] =
     for (Exn.Res((name, _)) <- blobs) yield name