src/Pure/Thy/thy_syntax.scala
changeset 40454 2516ea25a54b
parent 38878 1d5b3175fd30
child 40457 3b0050718b31
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Nov 10 11:44:35 2010 +0100
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Nov 10 15:00:40 2010 +0100
     1.3 @@ -13,6 +13,70 @@
     1.4  
     1.5  object Thy_Syntax
     1.6  {
     1.7 +  /** nested structure **/
     1.8 +
     1.9 +  object Structure
    1.10 +  {
    1.11 +    sealed abstract class Entry
    1.12 +    {
    1.13 +      def length: Int
    1.14 +    }
    1.15 +    case class Block(val name: String, val body: List[Entry]) extends Entry
    1.16 +    {
    1.17 +      val length: Int = (0 /: body)(_ + _.length)
    1.18 +    }
    1.19 +    case class Atom(val command: Command) extends Entry
    1.20 +    {
    1.21 +      def length: Int = command.length
    1.22 +    }
    1.23 +
    1.24 +    def parse_sections(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
    1.25 +    {
    1.26 +      /* stack operations */
    1.27 +
    1.28 +      def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
    1.29 +      var stack: List[(Int, String, mutable.ListBuffer[Entry])] = List((0, root_name, buffer()))
    1.30 +
    1.31 +      @tailrec def close(level: Int => Boolean)
    1.32 +      {
    1.33 +        stack match {
    1.34 +          case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
    1.35 +            body2 += Block(name, body.toList)
    1.36 +            stack = stack.tail
    1.37 +            close(level)
    1.38 +          case _ =>
    1.39 +        }
    1.40 +      }
    1.41 +
    1.42 +      def result(): Entry =
    1.43 +      {
    1.44 +        close(_ => true)
    1.45 +        val (_, name, body) = stack.head
    1.46 +        Block(name, body.toList)
    1.47 +      }
    1.48 +
    1.49 +      def add(command: Command)
    1.50 +      {
    1.51 +        syntax.heading_level(command) match {
    1.52 +          case Some(i) =>
    1.53 +            close(_ > i)
    1.54 +            stack = (i, command.source, buffer()) :: stack
    1.55 +          case None =>
    1.56 +        }
    1.57 +        stack.head._3 += Atom(command)
    1.58 +      }
    1.59 +
    1.60 +
    1.61 +      /* result structure */
    1.62 +
    1.63 +      val spans = parse_spans(syntax.scan(text))
    1.64 +      spans.foreach(span => add(Command.span(span)))
    1.65 +      result()
    1.66 +    }
    1.67 +  }
    1.68 +
    1.69 +
    1.70 +
    1.71    /** parse spans **/
    1.72  
    1.73    def parse_spans(toks: List[Token]): List[List[Token]] =