more command categories, as in ML;
authorwenzelm
Sun Mar 15 12:49:20 2015 +0100 (2015-03-15)
changeset 59700d887abcc7c24
parent 59699 a6efad6acafd
child 59701 8ab877c91992
more command categories, as in ML;
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
     1.1 --- a/src/Pure/Isar/keyword.scala	Sun Mar 15 12:42:30 2015 +0100
     1.2 +++ b/src/Pure/Isar/keyword.scala	Sun Mar 15 12:49:20 2015 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4    val PRF_SCRIPT = "prf_script"
     1.5  
     1.6  
     1.7 -  /* categories */
     1.8 +  /* command categories */
     1.9  
    1.10    val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
    1.11  
    1.12 @@ -50,6 +50,9 @@
    1.13    val document_raw = Set(DOCUMENT_RAW)
    1.14    val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
    1.15  
    1.16 +  val theory_begin = Set(THY_BEGIN)
    1.17 +  val theory_end = Set(THY_END)
    1.18 +
    1.19    val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
    1.20  
    1.21    val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Sun Mar 15 12:42:30 2015 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sun Mar 15 12:49:20 2015 +0100
     2.3 @@ -235,7 +235,7 @@
     2.4        case "subsubsection" => Some(3)
     2.5        case _ =>
     2.6          keywords.command_kind(command.name) match {
     2.7 -          case Some(kind) if Keyword.theory(kind) && kind != Keyword.THY_END => Some(4)
     2.8 +          case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(4)
     2.9            case _ => None
    2.10          }
    2.11      }