treat main theory commands like headings, and nest anything else inside;
authorwenzelm
Wed Nov 10 15:43:06 2010 +0100 (2010-11-10)
changeset 4045812c8c64203b3
parent 40457 3b0050718b31
child 40459 913e545d9a9b
treat main theory commands like headings, and nest anything else inside;
src/Pure/Isar/outer_syntax.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:42:20 2010 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:43:06 2010 +0100
     1.3 @@ -33,26 +33,30 @@
     1.4    def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
     1.5  
     1.6    def is_command(name: String): Boolean =
     1.7 -    keywords.get(name) match {
     1.8 +    keyword_kind(name) match {
     1.9        case Some(kind) => kind != Keyword.MINOR
    1.10        case None => false
    1.11      }
    1.12  
    1.13    def is_heading(name: String): Boolean =
    1.14 -    keywords.get(name) match {
    1.15 +    keyword_kind(name) match {
    1.16        case Some(kind) => Keyword.heading(kind)
    1.17        case None => false
    1.18      }
    1.19  
    1.20    def heading_level(name: String): Option[Int] =
    1.21      name match {
    1.22 -      // FIXME avoid hard-wired info
    1.23 +      // FIXME avoid hard-wired info!?
    1.24        case "header" => Some(1)
    1.25        case "chapter" => Some(2)
    1.26        case "section" | "sect" => Some(3)
    1.27        case "subsection" | "subsect" => Some(4)
    1.28        case "subsubsection" | "subsubsect" => Some(5)
    1.29 -      case _ => None
    1.30 +      case _ =>
    1.31 +        keyword_kind(name) match {
    1.32 +          case Some(kind) if Keyword.theory(kind) => Some(6)
    1.33 +          case _ => None
    1.34 +        }
    1.35      }
    1.36  
    1.37    def heading_level(command: Command): Option[Int] =
     2.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 15:42:20 2010 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 15:43:06 2010 +0100
     2.3 @@ -129,7 +129,7 @@
     2.4              })
     2.5            List(node)
     2.6          case Structure.Atom(command)
     2.7 -        if command.is_command && !syntax.is_heading(command.name) =>
     2.8 +        if command.is_command && syntax.heading_level(command).isEmpty =>
     2.9            val node =
    2.10              new DefaultMutableTreeNode(
    2.11                new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))