# HG changeset patch
# User wenzelm
# Date 1289398645 -3600
# Node ID e035dad8eca2960ab762512010e891d23d93c0ee
# Parent  2516ea25a54bea5af477747610f50dcd9d6c305c
default Sidekick parser based on section headings;

diff -r 2516ea25a54b -r e035dad8eca2 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:00:40 2010 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:17:25 2010 +0100
@@ -38,6 +38,12 @@
       case None => false
     }
 
+  def is_heading(name: String): Boolean =
+    keywords.get(name) match {
+      case Some(kind) => Keyword.heading(kind)
+      case None => false
+    }
+
   def heading_level(name: String): Option[Int] =
     name match {
       // FIXME avoid hard-wired info
diff -r 2516ea25a54b -r e035dad8eca2 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 15:00:40 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 15:17:25 2010 +0100
@@ -110,20 +110,38 @@
 
 class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
 {
+  import Thy_Syntax.Structure
+
   def parser(data: SideKickParsedData, model: Document_Model)
   {
-    val root = data.root
-    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
-    for {
-      (command, command_start) <- snapshot.node.command_range()
-      if command.is_command && !stopped
-    }
-    {
-      val node =
-        new DefaultMutableTreeNode(
-          new Isabelle_Sidekick.Asset(command.name, command_start, command_start + command.length))
-      root.add(node)
-    }
+    val syntax = model.session.current_syntax()
+
+    def make_tree(offset: Int, entry: Structure.Entry): List[DefaultMutableTreeNode] =
+      entry match {
+        case Structure.Block(name, body) =>
+          val node =
+            new DefaultMutableTreeNode(
+              new Isabelle_Sidekick.Asset(name, offset, offset + entry.length))
+          (offset /: body)((i, e) =>
+            {
+              make_tree(i, e) foreach (nd => node.add(nd))
+              i + e.length
+            })
+          List(node)
+        case Structure.Atom(command)
+        if command.is_command && !syntax.is_heading(command.name) =>
+          val node =
+            new DefaultMutableTreeNode(
+              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
+          List(node)
+        case _ => Nil
+      }
+
+    val buffer = model.buffer
+    val text = Isabelle.buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
+    val structure = Structure.parse_sections(syntax, "theory " + model.thy_name, text)
+
+    make_tree(0, structure) foreach (node => data.root.add(node))
   }
 }