diff -r e2b512024eab -r ba531af91148 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 07 15:01:48 2012 +0200
@@ -35,14 +35,18 @@
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
 
-  type Node_Header = Exn.Result[Node.Deps]
-
   object Node
   {
-    sealed case class Deps(
+    sealed case class Header(
       imports: List[Name],
       keywords: Thy_Header.Keywords,
-      uses: List[(String, Boolean)])
+      uses: List[(String, Boolean)],
+      errors: List[String] = Nil)
+    {
+      def error(msg: String): Header = copy(errors = errors ::: List(msg))
+    }
+
+    def bad_header(msg: String): Header = Header(Nil, Nil, Nil, List(msg))
 
     object Name
     {
@@ -83,7 +87,7 @@
     }
     case class Clear[A, B]() extends Edit[A, B]
     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
-    case class Header[A, B](header: Node_Header) extends Edit[A, B]
+    case class Deps[A, B](header: Header) extends Edit[A, B]
     case class Perspective[A, B](perspective: B) extends Edit[A, B]
 
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
@@ -103,14 +107,14 @@
   }
 
   final class Node private(
-    val header: Node_Header = Exn.Exn(ERROR("Bad theory header")),
+    val header: Node.Header = Node.bad_header("Bad theory header"),
     val perspective: Command.Perspective = Command.Perspective.empty,
     val blobs: Map[String, Blob] = Map.empty,
     val commands: Linear_Set[Command] = Linear_Set.empty)
   {
     def clear: Node = new Node(header = header)
 
-    def update_header(new_header: Node_Header): Node =
+    def update_header(new_header: Node.Header): Node =
       new Node(new_header, perspective, blobs, commands)
 
     def update_perspective(new_perspective: Command.Perspective): Node =
@@ -122,12 +126,6 @@
     def update_commands(new_commands: Linear_Set[Command]): Node =
       new Node(header, perspective, blobs, new_commands)
 
-    def imports: List[Node.Name] =
-      header match { case Exn.Res(deps) => deps.imports case _ => Nil }
-
-    def keywords: Thy_Header.Keywords =
-      header match { case Exn.Res(deps) => deps.keywords case _ => Nil }
-
 
     /* commands */
 
@@ -190,7 +188,7 @@
     def + (entry: (Node.Name, Node)): Nodes =
     {
       val (name, node) = entry
-      val imports = node.imports
+      val imports = node.header.imports
       val graph1 =
         (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
       val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))