# HG changeset patch
# User wenzelm
# Date 1413881604 -7200
# Node ID c07a59140feee9b72aff012531612bd65c93905a
# Parent  bb55a3530709db04fc54e38c257c3a7599957b8e
clarified tree root;

diff -r bb55a3530709 -r c07a59140fee src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 10:00:25 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 10:53:24 2014 +0200
@@ -293,7 +293,8 @@
     }
   }
 
-  def parse_document(node_name: Document.Node.Name, text: CharSequence): Outer_Syntax.Document =
+  def parse_document(node_name: Document.Node.Name, text: CharSequence):
+    List[Outer_Syntax.Document] =
   {
     /* stack operations */
 
@@ -301,7 +302,7 @@
       new mutable.ListBuffer[Outer_Syntax.Document]
 
     var stack: List[(Int, String, mutable.ListBuffer[Outer_Syntax.Document])] =
-      List((0, node_name.toString, buffer()))
+      List((0, "", buffer()))
 
     @tailrec def close(level: Int => Boolean)
     {
@@ -314,11 +315,10 @@
       }
     }
 
-    def result(): Outer_Syntax.Document =
+    def result(): List[Outer_Syntax.Document] =
     {
       close(_ => true)
-      val (_, name, body) = stack.head
-      Outer_Syntax.Document_Block(name, body.toList)
+      stack.head._3.toList
     }
 
     def add(command: Command)
diff -r bb55a3530709 -r c07a59140fee src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Oct 21 10:00:25 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Oct 21 10:53:24 2014 +0200
@@ -101,27 +101,28 @@
 {
   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   {
-    def make_tree(offset: Text.Offset, document: Outer_Syntax.Document)
-        : List[DefaultMutableTreeNode] =
-      document match {
-        case Outer_Syntax.Document_Block(name, body) =>
-          val node =
-            new DefaultMutableTreeNode(
-              new Isabelle_Sidekick.Asset(
-                Library.first_line(name), offset, offset + document.length))
-          (offset /: body)((i, doc) =>
-            {
-              for (nd <- make_tree(i, doc)) node.add(nd)
-              i + doc.length
-            })
-          List(node)
-        case _ => Nil
+    def make_tree(
+      parent: DefaultMutableTreeNode,
+      offset: Text.Offset,
+      documents: List[Outer_Syntax.Document])
+    {
+      (offset /: documents) { case (i, document) =>
+        document match {
+          case Outer_Syntax.Document_Block(name, body) =>
+            val node =
+              new DefaultMutableTreeNode(
+                new Isabelle_Sidekick.Asset(Library.first_line(name), i, i + document.length))
+            parent.add(node)
+            make_tree(node, i, body)
+          case _ =>
+        }
+        i + document.length
       }
+    }
 
     node_name(buffer) match {
       case Some(name) =>
-        val document = syntax.parse_document(name, JEdit_Lib.buffer_text(buffer))
-        for (node <- make_tree(0, document)) data.root.add(node)
+        make_tree(data.root, 0, syntax.parse_document(name, JEdit_Lib.buffer_text(buffer)))
         true
       case None => false
     }