diff -r 8ab877c91992 -r 58dfaa369c11 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sun Mar 15 14:46:01 2015 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Mar 15 19:21:15 2015 +0100
@@ -143,8 +143,8 @@
 
   @tailrec private def chop_common(
       cmds: List[Command],
-      blobs_spans: List[((List[Command.Blob], Int), Command_Span.Span)])
-    : (List[Command], List[((List[Command.Blob], Int), Command_Span.Span)]) =
+      blobs_spans: List[(Command.Blobs_Info, Command_Span.Span)])
+    : (List[Command], List[(Command.Blobs_Info, Command_Span.Span)]) =
   {
     (cmds, blobs_spans) match {
       case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
@@ -157,14 +157,17 @@
     resources: Resources,
     syntax: Prover.Syntax,
     get_blob: Document.Node.Name => Option[Document.Blob],
+    can_import: Document.Node.Name => Boolean,
     node_name: Document.Node.Name,
+    header: Document.Node.Header,
     commands: Linear_Set[Command],
     first: Command, last: Command): Linear_Set[Command] =
   {
     val cmds0 = commands.iterator(first, last).toList
     val blobs_spans0 =
-      syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
-        map(span => (Command.resolve_files(resources, syntax, get_blob, node_name, span), span))
+      syntax.parse_spans(cmds0.iterator.map(_.source).mkString).map(span =>
+        (Command.blobs_info(resources, syntax, get_blob, can_import, node_name, header, span),
+          span))
 
     val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
 
@@ -180,7 +183,7 @@
         val hook = commands.prev(cmd)
         val inserted =
           blobs_spans2.map({ case (blobs, span) =>
-            Command(Document_ID.make(), node_name, Some(blobs), span) })
+            Command(Document_ID.make(), node_name, blobs, span) })
         (commands /: cmds2)(_ - _).append_after(hook, inserted)
     }
   }
@@ -193,7 +196,9 @@
     resources: Resources,
     syntax: Prover.Syntax,
     get_blob: Document.Node.Name => Option[Document.Blob],
-    name: Document.Node.Name,
+    can_import: Document.Node.Name => Boolean,
+    node_name: Document.Node.Name,
+    header: Document.Node.Header,
     perspective: Command.Perspective,
     commands: Linear_Set[Command]): Linear_Set[Command] =
   {
@@ -208,7 +213,8 @@
         case Some(first_unparsed) =>
           val first = next_invisible_command(cmds.reverse, first_unparsed)
           val last = next_invisible_command(cmds, first_unparsed)
-          recover(reparse_spans(resources, syntax, get_blob, name, cmds, first, last))
+          recover(reparse_spans(
+            resources, syntax, get_blob, can_import, node_name, header, cmds, first, last))
         case None => cmds
       }
     recover(commands)
@@ -221,8 +227,10 @@
     resources: Resources,
     syntax: Prover.Syntax,
     get_blob: Document.Node.Name => Option[Document.Blob],
+    can_import: Document.Node.Name => Boolean,
     reparse_limit: Int,
-    name: Document.Node.Name,
+    node_name: Document.Node.Name,
+    header: Document.Node.Header,
     perspective: Command.Perspective,
     commands: Linear_Set[Command]): Linear_Set[Command] =
   {
@@ -240,7 +248,8 @@
                 last = it.next
                 i += last.length
               }
-              reparse_spans(resources, syntax, get_blob, name, commands, first_unfinished, last)
+              reparse_spans(resources, syntax, get_blob, can_import, node_name,
+                header, commands, first_unfinished, last)
             case None => commands
           }
         case None => commands
@@ -265,6 +274,7 @@
     resources: Resources,
     syntax: Prover.Syntax,
     get_blob: Document.Node.Name => Option[Document.Blob],
+    can_import: Document.Node.Name => Boolean,
     reparse_limit: Int,
     node: Document.Node, edit: Document.Edit_Text): Document.Node =
   {
@@ -278,7 +288,8 @@
           val commands0 = node.commands
           val commands1 = edit_text(text_edits, commands0)
           val commands2 =
-            recover_spans(resources, syntax, get_blob, name, node.perspective.visible, commands1)
+            recover_spans(resources, syntax, get_blob, can_import, name,
+              node.header, node.perspective.visible, commands1)
           node.update_commands(commands2)
         }
         else node
@@ -293,8 +304,8 @@
         else
           node.update_perspective(text_perspective, perspective).
             update_commands(
-              consolidate_spans(resources, syntax, get_blob, reparse_limit,
-                name, visible, node.commands))
+              consolidate_spans(resources, syntax, get_blob, can_import, reparse_limit,
+                name, node.header, visible, node.commands))
     }
   }
 
@@ -305,10 +316,13 @@
       doc_blobs: Document.Blobs,
       edits: List[Document.Edit_Text]): Session.Change =
   {
+    val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
+
     def get_blob(name: Document.Node.Name) =
       doc_blobs.get(name) orElse previous.nodes(name).get_blob
 
-    val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
+    def can_import(name: Document.Node.Name): Boolean =
+      resources.loaded_theories(name.theory) || nodes0(name).has_header
 
     val (doc_edits, version) =
       if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
@@ -338,14 +352,15 @@
             val node1 =
               if (reparse_set(name) && commands.nonEmpty)
                 node.update_commands(
-                  reparse_spans(resources, syntax, get_blob,
-                    name, commands, commands.head, commands.last))
+                  reparse_spans(resources, syntax, get_blob, can_import, name,
+                    node.header, commands, commands.head, commands.last))
               else node
             val node2 =
-              (node1 /: edits)(text_edit(resources, syntax, get_blob, reparse_limit, _, _))
+              (node1 /: edits)(
+                text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _))
             val node3 =
               if (reparse_set.contains(name))
-                text_edit(resources, syntax, get_blob, reparse_limit,
+                text_edit(resources, syntax, get_blob, can_import, reparse_limit,
                   node2, (name, node2.edit_perspective))
               else node2