--- a/src/Pure/Isar/keyword.scala Sun Mar 15 12:42:30 2015 +0100
+++ b/src/Pure/Isar/keyword.scala Sun Mar 15 12:49:20 2015 +0100
@@ -39,7 +39,7 @@
val PRF_SCRIPT = "prf_script"
- /* categories */
+ /* command categories */
val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
@@ -50,6 +50,9 @@
val document_raw = Set(DOCUMENT_RAW)
val document = Set(DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
+ val theory_begin = Set(THY_BEGIN)
+ val theory_end = Set(THY_END)
+
val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
--- a/src/Pure/Isar/outer_syntax.scala Sun Mar 15 12:42:30 2015 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Sun Mar 15 12:49:20 2015 +0100
@@ -235,7 +235,7 @@
case "subsubsection" => Some(3)
case _ =>
keywords.command_kind(command.name) match {
- case Some(kind) if Keyword.theory(kind) && kind != Keyword.THY_END => Some(4)
+ case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(4)
case _ => None
}
}