# HG changeset patch
# User wenzelm
# Date 1289400140 -3600
# Node ID 3b0050718b315f0c1a87c0d743ea419493727e58
# Parent  e91b3c2145b46964b8b0e6daada1440ddb218715
proper treatment of equal heading level;

diff -r e91b3c2145b4 -r 3b0050718b31 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Nov 10 15:41:29 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Nov 10 15:42:20 2010 +0100
@@ -59,7 +59,7 @@
       {
         syntax.heading_level(command) match {
           case Some(i) =>
-            close(_ > i)
+            close(_ >= i)
             stack = (i, command.source, buffer()) :: stack
           case None =>
         }