# HG changeset patch
# User wenzelm
# Date 1412507784 -7200
# Node ID 19e062fbfea00f0150c26addfeb656037df3ff68
# Parent  48e23e34241517106c05736794ec6dbad12391c9
more advanced NEWS tree structure and folding;

diff -r 48e23e342415 -r 19e062fbfea0 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Sat Oct 04 22:15:31 2014 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Sun Oct 05 13:16:24 2014 +0200
@@ -72,7 +72,7 @@
 isabelle-timing.title=Timing
 
 #SideKick
-mode.isabelle-news.folding=none
+mode.isabelle-news.folding=sidekick
 mode.isabelle-news.sidekick.parser=isabelle-news
 mode.isabelle-options.folding=sidekick
 mode.isabelle-options.sidekick.parser=isabelle-options
@@ -84,6 +84,6 @@
 mode.isabelle.sidekick.showStatusWindow.label=true
 mode.ml.sidekick.parser=isabelle
 sidekick.parser.isabelle.label=Isabelle
+mode.bibtex.folding=sidekick
 mode.bibtex.sidekick.parser=bibtex
-mode.bibtex.folding=sidekick
 
diff -r 48e23e342415 -r 19e062fbfea0 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Oct 04 22:15:31 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sun Oct 05 13:16:24 2014 +0200
@@ -199,18 +199,44 @@
   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   {
     var offset = 0
+    var end_offset = 0
+
+    var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None
+    var start2: Option[(Int, String)] = None
+
+    def close1: Unit =
+      start1 match {
+        case Some((start_offset, s, body)) =>
+          val node = make_node(s, start_offset, end_offset)
+          body.foreach(node.add(_))
+          data.root.add(node)
+          start1 = None
+        case None =>
+      }
+
+    def close2: Unit =
+      start2 match {
+        case Some((start_offset, s)) =>
+          start1 match {
+            case Some((start_offset1, s1, body)) =>
+              val node = make_node(s, start_offset, end_offset)
+              start1 = Some((start_offset1, s1, body :+ node))
+            case None =>
+          }
+          start2 = None
+        case None =>
+      }
 
     for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
       line match {
-        case Heading1(s) =>
-          data.root.add(make_node(s, offset, offset + line.length))
-        case Heading2(s) =>
-          data.root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
-            .add(make_node(s, offset, offset + line.length))
+        case Heading1(s) => close2; close1; start1 = Some((offset, s, Vector()))
+        case Heading2(s) => close2; start2 = Some((offset, s))
         case _ =>
       }
       offset += line.length + 1
+      if (!line.forall(Character.isSpaceChar(_))) end_offset = offset
     }
+    if (!stopped) { close2; close1 }
 
     true
   }