clarified handling of plain theory commands;

--- a/src/Pure/Isar/document_structure.scala	Thu Aug 04 20:55:36 2016 +0200
+++ b/src/Pure/Isar/document_structure.scala	Thu Aug 04 21:21:31 2016 +0200
@@ -51,6 +51,11 @@
     node_name: Document.Node.Name,
     text: CharSequence): List[Document] =
   {
+    def is_plain_theory(command: Command): Boolean =
+      is_theory_command(syntax.keywords, command.span.name) &&
+      !command.span.is_begin && !command.span.is_end
+
+
     /* stack operations */
 
     def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
@@ -58,6 +63,8 @@
     var stack: List[(Command, mutable.ListBuffer[Document])] =
       List((Command.empty, buffer()))
 
+    def open(command: Command) { stack = (command, buffer()) :: stack }
+
     def close(): Boolean =
       stack match {
         case (command, body) :: (_, body2) :: _ =>
@@ -68,6 +75,8 @@
           false
       }
 
+    def flush() { if (is_plain_theory(stack.head._1)) close() }
+
     def result(): List[Document] =
     {
       while (close()) { }
@@ -76,8 +85,8 @@
 
     def add(command: Command)
     {
-      if (command.span.is_begin) stack = (command, buffer()) :: stack
-      else if (command.span.is_end) close()
+      if (command.span.is_begin || is_plain_theory(command)) { flush(); open(command) }
+      else if (command.span.is_end) { flush(); close() }
 
       stack.head._2 += Atom(command)
     }