treat main theory commands like headings, and nest anything else inside;

--- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:42:20 2010 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:43:06 2010 +0100
@@ -33,26 +33,30 @@
   def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
 
   def is_command(name: String): Boolean =
-    keywords.get(name) match {
+    keyword_kind(name) match {
       case Some(kind) => kind != Keyword.MINOR
       case None => false
     }
 
   def is_heading(name: String): Boolean =
-    keywords.get(name) match {
+    keyword_kind(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
+      // FIXME avoid hard-wired info!?
       case "header" => Some(1)
       case "chapter" => Some(2)
       case "section" | "sect" => Some(3)
       case "subsection" | "subsect" => Some(4)
       case "subsubsection" | "subsubsect" => Some(5)
-      case _ => None
+      case _ =>
+        keyword_kind(name) match {
+          case Some(kind) if Keyword.theory(kind) => Some(6)
+          case _ => None
+        }
     }
 
   def heading_level(command: Command): Option[Int] =

--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 15:42:20 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 15:43:06 2010 +0100
@@ -129,7 +129,7 @@
             })
           List(node)
         case Structure.Atom(command)
-        if command.is_command && !syntax.is_heading(command.name) =>
+        if command.is_command && syntax.heading_level(command).isEmpty =>
           val node =
             new DefaultMutableTreeNode(
               new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))