--- a/src/Pure/Thy/thy_structure.scala Sat Oct 18 22:50:35 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,71 +0,0 @@
-/* Title: Pure/Thy/thy_structure.scala
- Author: Makarius
-
-Nested structure of theory source.
-*/
-
-package isabelle
-
-
-import scala.collection.mutable
-import scala.annotation.tailrec
-
-
-object Thy_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(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence): Entry =
- {
- /* stack operations */
-
- def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
- var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
- List((0, node_name.toString, 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 + 1, command.source, 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, Nil, span)))
- result()
- }
-}
-