src/Pure/Isar/outer_syntax.scala
changeset 63460 f41070510341
parent 63459 8d68204d97d7
child 63479 464ef556bd21
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 14:13:42 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 14:51:39 2016 +0200
     1.3 @@ -142,6 +142,9 @@
     1.4  
     1.5    /* line-oriented structure */
     1.6  
     1.7 +  private val close_structure =
     1.8 +    Set(Keyword.NEXT_BLOCK, Keyword.QED_BLOCK, Keyword.PRF_CLOSE)
     1.9 +
    1.10    def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure)
    1.11      : Outer_Syntax.Line_Structure =
    1.12    {
    1.13 @@ -151,9 +154,7 @@
    1.14      val command_depth =
    1.15        tokens.iterator.filter(_.is_proper).toStream.headOption match {
    1.16          case Some(tok) =>
    1.17 -          if (keywords.is_command(tok, Keyword.QED_BLOCK == _))
    1.18 -            Some(structure.after_span_depth - 2)
    1.19 -          else if (keywords.is_command(tok, Keyword.PRF_CLOSE == _))
    1.20 +          if (keywords.is_command(tok, close_structure))
    1.21              Some(structure.after_span_depth - 1)
    1.22            else None
    1.23          case None => None