src/Pure/Isar/outer_syntax.scala
changeset 58747 c680f181b32e
parent 58743 c07a59140fee
child 58748 8f92f17d8781
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 13:21:59 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 13:56:42 2014 +0200
     1.3 @@ -63,11 +63,11 @@
     1.4    /* overall document structure */
     1.5  
     1.6    sealed abstract class Document { def length: Int }
     1.7 -  case class Document_Block(val name: String, val body: List[Document]) extends Document
     1.8 +  case class Document_Block(name: String, text: String, body: List[Document]) extends Document
     1.9    {
    1.10      val length: Int = (0 /: body)(_ + _.length)
    1.11    }
    1.12 -  case class Document_Atom(val command: Command) extends Document
    1.13 +  case class Document_Atom(command: Command) extends Document
    1.14    {
    1.15      def length: Int = command.length
    1.16    }
    1.17 @@ -301,14 +301,14 @@
    1.18      def buffer(): mutable.ListBuffer[Outer_Syntax.Document] =
    1.19        new mutable.ListBuffer[Outer_Syntax.Document]
    1.20  
    1.21 -    var stack: List[(Int, String, mutable.ListBuffer[Outer_Syntax.Document])] =
    1.22 -      List((0, "", buffer()))
    1.23 +    var stack: List[(Int, Command, mutable.ListBuffer[Outer_Syntax.Document])] =
    1.24 +      List((0, Command.empty, buffer()))
    1.25  
    1.26      @tailrec def close(level: Int => Boolean)
    1.27      {
    1.28        stack match {
    1.29 -        case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
    1.30 -          body2 += Outer_Syntax.Document_Block(name, body.toList)
    1.31 +        case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
    1.32 +          body2 += Outer_Syntax.Document_Block(command.name, command.source, body.toList)
    1.33            stack = stack.tail
    1.34            close(level)
    1.35          case _ =>
    1.36 @@ -326,7 +326,7 @@
    1.37        heading_level(command) match {
    1.38          case Some(i) =>
    1.39            close(_ > i)
    1.40 -          stack = (i + 1, command.source, buffer()) :: stack
    1.41 +          stack = (i + 1, command, buffer()) :: stack
    1.42          case None =>
    1.43        }
    1.44        stack.head._3 += Outer_Syntax.Document_Atom(command)