src/Pure/Isar/document_structure.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/document_structure.scala	Thu Aug 04 11:17:11 2016 +0200
@@ -0,0 +1,90 @@
+/*  Title:      Pure/Isar/document_structure.scala
+    Author:     Makarius
+
+Overall document structure.
+*/
+
+package isabelle
+
+
+import scala.collection.mutable
+import scala.annotation.tailrec
+
+
+object Document_Structure
+{
+  /** section headings etc. **/
+
+  sealed abstract class Document { def length: Int }
+  case class Block(name: String, text: String, body: List[Document]) extends Document
+  { val length: Int = (0 /: body)(_ + _.length) }
+  case class Atom(command: Command) extends Document
+  { def length: Int = command.length }
+
+  def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
+  {
+    val name = command.span.name
+    name match {
+      case Thy_Header.CHAPTER => Some(0)
+      case Thy_Header.SECTION => Some(1)
+      case Thy_Header.SUBSECTION => Some(2)
+      case Thy_Header.SUBSUBSECTION => Some(3)
+      case Thy_Header.PARAGRAPH => Some(4)
+      case Thy_Header.SUBPARAGRAPH => Some(5)
+      case _ =>
+        keywords.kinds.get(name) match {
+          case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
+          case _ => None
+        }
+    }
+  }
+
+  def parse_document(
+    syntax: Outer_Syntax,
+    node_name: Document.Node.Name,
+    text: CharSequence): List[Document] =
+  {
+    /* stack operations */
+
+    def buffer(): mutable.ListBuffer[Document] =
+      new mutable.ListBuffer[Document]
+
+    var stack: List[(Int, Command, mutable.ListBuffer[Document])] =
+      List((0, Command.empty, buffer()))
+
+    @tailrec def close(level: Int => Boolean)
+    {
+      stack match {
+        case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
+          body2 += Block(command.span.name, command.source, body.toList)
+          stack = stack.tail
+          close(level)
+        case _ =>
+      }
+    }
+
+    def result(): List[Document] =
+    {
+      close(_ => true)
+      stack.head._3.toList
+    }
+
+    def add(command: Command)
+    {
+      heading_level(syntax.keywords, command) match {
+        case Some(i) =>
+          close(_ > i)
+          stack = (i + 1, command, buffer()) :: stack
+        case None =>
+      }
+      stack.head._3 += Atom(command)
+    }
+
+
+    /* result structure */
+
+    val spans = syntax.parse_spans(text)
+    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
+    result()
+  }
+}