src/Pure/PIDE/document.scala

     /* header and name */
 
     sealed case class Header(
       imports: List[Name],
       keywords: Thy_Header.Keywords,
-      errors: List[String] = Nil)
+      errors: List[String])
     {
       def error(msg: String): Header = copy(errors = errors ::: List(msg))
 
       def cat_errors(msg2: String): Header =
         copy(errors = errors.map(msg1 => Library.cat_message(msg1, msg2)))
     }
 
+    val no_header = Header(Nil, Nil, Nil)
     def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
-
-    val no_header = bad_header("No theory header")
 
     object Name
     {
       val empty = Name("")
 

     /* perspective */
 
     type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
     type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
 
-    val empty_perspective_text: Perspective_Text =
+    val no_perspective_text: Perspective_Text =
       Perspective(false, Text.Perspective.empty, Overlays.empty)
 
-    val empty_perspective_command: Perspective_Command =
+    val no_perspective_command: Perspective_Command =
       Perspective(false, Command.Perspective.empty, Overlays.empty)
+
+    def is_no_perspective_command(perspective: Perspective_Command): Boolean =
+      !perspective.required &&
+      perspective.visible.is_empty &&
+      perspective.overlays.is_empty
 
 
     /* commands */
 
     object Commands

     val empty: Node = new Node()
   }
 
   final class Node private(
     val get_blob: Option[Document.Blob] = None,
-    val header: Node.Header = Node.bad_header("Bad theory header"),
-    val perspective: Node.Perspective_Command = Node.empty_perspective_command,
+    val header: Node.Header = Node.no_header,
+    val perspective: Node.Perspective_Command = Node.no_perspective_command,
     _commands: Node.Commands = Node.Commands.empty)
   {
+    def is_empty: Boolean =
+      get_blob.isEmpty &&
+      header == Node.no_header &&
+      Node.is_no_perspective_command(perspective) &&
+      commands.isEmpty
+
+    def commands: Linear_Set[Command] = _commands.commands
+    def load_commands: List[Command] = _commands.load_commands
+
     def clear: Node = new Node(header = header)
 
     def init_blob(blob: Document.Blob): Node = new Node(Some(blob.unchanged))
 
     def update_header(new_header: Node.Header): Node =

 
     def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
       perspective.required == other_perspective.required &&
       perspective.visible.same(other_perspective.visible) &&
       perspective.overlays == other_perspective.overlays
-
-    def commands: Linear_Set[Command] = _commands.commands
-    def load_commands: List[Command] = _commands.load_commands
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
       else new Node(get_blob, header, perspective, Node.Commands(new_commands))