proper treatment of equal heading level;
authorwenzelm
Wed Nov 10 15:42:20 2010 +0100 (2010-11-10)
changeset 404573b0050718b31
parent 40456 e91b3c2145b4
child 40458 12c8c64203b3
proper treatment of equal heading level;
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Nov 10 15:41:29 2010 +0100
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Nov 10 15:42:20 2010 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4        {
     1.5          syntax.heading_level(command) match {
     1.6            case Some(i) =>
     1.7 -            close(_ > i)
     1.8 +            close(_ >= i)
     1.9              stack = (i, command.source, buffer()) :: stack
    1.10            case None =>
    1.11          }