src/Pure/Isar/line_structure.scala
changeset 66177 7fd83f20e3e9
parent 63603 9d9ea2c6bc38
child 68730 0bc491938780
     1.1 --- a/src/Pure/Isar/line_structure.scala	Fri Jun 23 14:38:32 2017 +0200
     1.2 +++ b/src/Pure/Isar/line_structure.scala	Fri Jun 23 14:59:00 2017 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4  
     1.5  sealed case class Line_Structure(
     1.6    improper: Boolean = true,
     1.7 +  blank: Boolean = true,
     1.8    command: Boolean = false,
     1.9    depth: Int = 0,
    1.10    span_depth: Int = 0,
    1.11 @@ -23,6 +24,7 @@
    1.12    def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure =
    1.13    {
    1.14      val improper1 = tokens.forall(_.is_improper)
    1.15 +    val blank1 = tokens.forall(_.is_space)
    1.16      val command1 = tokens.exists(_.is_begin_or_command)
    1.17  
    1.18      val command_depth =
    1.19 @@ -62,6 +64,7 @@
    1.20            else depths
    1.21        }
    1.22  
    1.23 -    Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
    1.24 +    Line_Structure(
    1.25 +      improper1, blank1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
    1.26    }
    1.27  }