--- a/src/Pure/Thy/thy_syntax.scala Wed Nov 10 11:44:35 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Wed Nov 10 15:00:40 2010 +0100
@@ -13,6 +13,70 @@
object Thy_Syntax
{
+ /** nested structure **/
+
+ object Structure
+ {
+ sealed abstract class Entry
+ {
+ def length: Int
+ }
+ case class Block(val name: String, val body: List[Entry]) extends Entry
+ {
+ val length: Int = (0 /: body)(_ + _.length)
+ }
+ case class Atom(val command: Command) extends Entry
+ {
+ def length: Int = command.length
+ }
+
+ def parse_sections(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
+ {
+ /* stack operations */
+
+ def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
+ var stack: List[(Int, String, mutable.ListBuffer[Entry])] = List((0, root_name, buffer()))
+
+ @tailrec def close(level: Int => Boolean)
+ {
+ stack match {
+ case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
+ body2 += Block(name, body.toList)
+ stack = stack.tail
+ close(level)
+ case _ =>
+ }
+ }
+
+ def result(): Entry =
+ {
+ close(_ => true)
+ val (_, name, body) = stack.head
+ Block(name, body.toList)
+ }
+
+ def add(command: Command)
+ {
+ syntax.heading_level(command) match {
+ case Some(i) =>
+ close(_ > i)
+ stack = (i, command.source, buffer()) :: stack
+ case None =>
+ }
+ stack.head._3 += Atom(command)
+ }
+
+
+ /* result structure */
+
+ val spans = parse_spans(syntax.scan(text))
+ spans.foreach(span => add(Command.span(span)))
+ result()
+ }
+ }
+
+
+
/** parse spans **/
def parse_spans(toks: List[Token]): List[List[Token]] =