# HG changeset patch
# User wenzelm
# Date 1289397640 -3600
# Node ID 2516ea25a54bea5af477747610f50dcd9d6c305c
# Parent  a81346e57ceff95b83faa556a803cf0bbb79100e
some support for nested source structure, based on section headings;

diff -r a81346e57cef -r 2516ea25a54b src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 11:44:35 2010 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:00:40 2010 +0100
@@ -38,6 +38,20 @@
       case None => false
     }
 
+  def heading_level(name: String): Option[Int] =
+    name match {
+      // FIXME avoid hard-wired info
+      case "header" => Some(1)
+      case "chapter" => Some(2)
+      case "section" | "sect" => Some(3)
+      case "subsection" | "subsect" => Some(4)
+      case "subsubsection" | "subsubsect" => Some(5)
+      case _ => None
+    }
+
+  def heading_level(command: Command): Option[Int] =
+    heading_level(command.name)
+
 
   /* tokenize */
 
diff -r a81346e57cef -r 2516ea25a54b src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Nov 10 11:44:35 2010 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Nov 10 15:00:40 2010 +0100
@@ -74,10 +74,13 @@
   }
 
 
-  /* unparsed dummy commands */
+  /* dummy commands */
 
-  def unparsed(source: String) =
+  def unparsed(source: String): Command =
     new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
+
+  def span(toks: List[Token]): Command =
+    new Command(Document.NO_ID, toks)
 }
 
 
diff -r a81346e57cef -r 2516ea25a54b src/Pure/Thy/thy_syntax.scala
--- 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]] =