diff -r a6efad6acafd -r d887abcc7c24 src/Pure/Isar/keyword.scala --- 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)