src/Pure/Isar/outer_syntax.scala
changeset 63460 f41070510341
parent 63459 8d68204d97d7
child 63479 464ef556bd21
--- 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