--- 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)
}