src/Pure/Isar/outer_syntax.scala
changeset 58743 c07a59140fee
parent 58706 70a947611792
child 58747 c680f181b32e
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 10:00:25 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 10:53:24 2014 +0200
     1.3 @@ -293,7 +293,8 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def parse_document(node_name: Document.Node.Name, text: CharSequence): Outer_Syntax.Document =
     1.8 +  def parse_document(node_name: Document.Node.Name, text: CharSequence):
     1.9 +    List[Outer_Syntax.Document] =
    1.10    {
    1.11      /* stack operations */
    1.12  
    1.13 @@ -301,7 +302,7 @@
    1.14        new mutable.ListBuffer[Outer_Syntax.Document]
    1.15  
    1.16      var stack: List[(Int, String, mutable.ListBuffer[Outer_Syntax.Document])] =
    1.17 -      List((0, node_name.toString, buffer()))
    1.18 +      List((0, "", buffer()))
    1.19  
    1.20      @tailrec def close(level: Int => Boolean)
    1.21      {
    1.22 @@ -314,11 +315,10 @@
    1.23        }
    1.24      }
    1.25  
    1.26 -    def result(): Outer_Syntax.Document =
    1.27 +    def result(): List[Outer_Syntax.Document] =
    1.28      {
    1.29        close(_ => true)
    1.30 -      val (_, name, body) = stack.head
    1.31 -      Outer_Syntax.Document_Block(name, body.toList)
    1.32 +      stack.head._3.toList
    1.33      }
    1.34  
    1.35      def add(command: Command)