src/Pure/Isar/outer_syntax.scala
changeset 59939 7d46aa03696e
parent 59924 801b979ec0c2
child 60215 5fb4990dfc73
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Apr 06 17:28:07 2015 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Apr 06 22:11:01 2015 +0200
     1.3 @@ -219,8 +219,8 @@
     1.4  
     1.5      for (tok <- toks) {
     1.6        if (tok.is_improper) improper += tok
     1.7 -      else if (tok.is_private ||
     1.8 -        tok.is_command && (!content.exists(_.is_private) || content.exists(_.is_command)))
     1.9 +      else if (tok.is_command_modifier ||
    1.10 +        tok.is_command && (!content.exists(_.is_command_modifier) || content.exists(_.is_command)))
    1.11        { flush(); content += tok }
    1.12        else { content ++= improper; improper.clear; content += tok }
    1.13      }