# HG changeset patch
# User wenzelm
# Date 1468327899 -7200
# Node ID f410705103414d963d94182c754bbdd56d7b7793
# Parent  8d68204d97d7d97fa8541b9060cb8b6785544d1e
clarified;

diff -r 8d68204d97d7 -r f41070510341 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 14:13:42 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 14:51:39 2016 +0200
@@ -142,6 +142,9 @@
 
   /* line-oriented structure */
 
+  private val close_structure =
+    Set(Keyword.NEXT_BLOCK, Keyword.QED_BLOCK, Keyword.PRF_CLOSE)
+
   def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure)
     : Outer_Syntax.Line_Structure =
   {
@@ -151,9 +154,7 @@
     val command_depth =
       tokens.iterator.filter(_.is_proper).toStream.headOption match {
         case Some(tok) =>
-          if (keywords.is_command(tok, Keyword.QED_BLOCK == _))
-            Some(structure.after_span_depth - 2)
-          else if (keywords.is_command(tok, Keyword.PRF_CLOSE == _))
+          if (keywords.is_command(tok, close_structure))
             Some(structure.after_span_depth - 1)
           else None
         case None => None