--- a/src/Pure/Isar/line_structure.scala Fri Jun 23 14:38:32 2017 +0200
+++ b/src/Pure/Isar/line_structure.scala Fri Jun 23 14:59:00 2017 +0200
@@ -14,6 +14,7 @@
sealed case class Line_Structure(
improper: Boolean = true,
+ blank: Boolean = true,
command: Boolean = false,
depth: Int = 0,
span_depth: Int = 0,
@@ -23,6 +24,7 @@
def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure =
{
val improper1 = tokens.forall(_.is_improper)
+ val blank1 = tokens.forall(_.is_space)
val command1 = tokens.exists(_.is_begin_or_command)
val command_depth =
@@ -62,6 +64,7 @@
else depths
}
- Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
+ Line_Structure(
+ improper1, blank1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
}
}