src/Pure/Isar/outer_syntax.scala
changeset 63441 4c3fa4dba79f
parent 63429 baedd4724f08
child 63458 723f9c673c1c
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Jul 11 14:25:06 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Jul 11 16:36:29 2016 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  
     1.5    /* load commands */
     1.6  
     1.7 -  def load_command(name: String): Option[List[String]] = keywords.load_command(name)
     1.8 +  def load_command(name: String): Option[List[String]] = keywords.load_commands.get(name)
     1.9    def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
    1.10  
    1.11  
    1.12 @@ -209,8 +209,9 @@
    1.13  
    1.14      for (tok <- toks) {
    1.15        if (tok.is_improper) improper += tok
    1.16 -      else if (tok.is_command_modifier ||
    1.17 -        tok.is_command && (!content.exists(_.is_command_modifier) || content.exists(_.is_command)))
    1.18 +      else if (keywords.is_before_command(tok) ||
    1.19 +        tok.is_command &&
    1.20 +          (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
    1.21        { flush(); content += tok }
    1.22        else { content ++= improper; improper.clear; content += tok }
    1.23      }
    1.24 @@ -236,7 +237,7 @@
    1.25        case Thy_Header.PARAGRAPH => Some(4)
    1.26        case Thy_Header.SUBPARAGRAPH => Some(5)
    1.27        case _ =>
    1.28 -        keywords.command_kind(name) match {
    1.29 +        keywords.kinds.get(name) match {
    1.30            case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
    1.31            case _ => None
    1.32          }