clarified tree root;
authorwenzelm
Tue Oct 21 10:53:24 2014 +0200 (2014-10-21)
changeset 58743c07a59140fee
parent 58742 bb55a3530709
child 58744 c434e37f290e
clarified tree root;
src/Pure/Isar/outer_syntax.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
     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)
     2.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Oct 21 10:00:25 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Oct 21 10:53:24 2014 +0200
     2.3 @@ -101,27 +101,28 @@
     2.4  {
     2.5    override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
     2.6    {
     2.7 -    def make_tree(offset: Text.Offset, document: Outer_Syntax.Document)
     2.8 -        : List[DefaultMutableTreeNode] =
     2.9 -      document match {
    2.10 -        case Outer_Syntax.Document_Block(name, body) =>
    2.11 -          val node =
    2.12 -            new DefaultMutableTreeNode(
    2.13 -              new Isabelle_Sidekick.Asset(
    2.14 -                Library.first_line(name), offset, offset + document.length))
    2.15 -          (offset /: body)((i, doc) =>
    2.16 -            {
    2.17 -              for (nd <- make_tree(i, doc)) node.add(nd)
    2.18 -              i + doc.length
    2.19 -            })
    2.20 -          List(node)
    2.21 -        case _ => Nil
    2.22 +    def make_tree(
    2.23 +      parent: DefaultMutableTreeNode,
    2.24 +      offset: Text.Offset,
    2.25 +      documents: List[Outer_Syntax.Document])
    2.26 +    {
    2.27 +      (offset /: documents) { case (i, document) =>
    2.28 +        document match {
    2.29 +          case Outer_Syntax.Document_Block(name, body) =>
    2.30 +            val node =
    2.31 +              new DefaultMutableTreeNode(
    2.32 +                new Isabelle_Sidekick.Asset(Library.first_line(name), i, i + document.length))
    2.33 +            parent.add(node)
    2.34 +            make_tree(node, i, body)
    2.35 +          case _ =>
    2.36 +        }
    2.37 +        i + document.length
    2.38        }
    2.39 +    }
    2.40  
    2.41      node_name(buffer) match {
    2.42        case Some(name) =>
    2.43 -        val document = syntax.parse_document(name, JEdit_Lib.buffer_text(buffer))
    2.44 -        for (node <- make_tree(0, document)) data.root.add(node)
    2.45 +        make_tree(data.root, 0, syntax.parse_document(name, JEdit_Lib.buffer_text(buffer)))
    2.46          true
    2.47        case None => false
    2.48      }