# HG changeset patch
# User wenzelm
# Date 1498222740 -7200
# Node ID 7fd83f20e3e914deaacc8142439613bd717ccae4
# Parent  b51a40281016a2163796a9d3defaa85258d53944
more information;

diff -r b51a40281016 -r 7fd83f20e3e9 src/Pure/Isar/line_structure.scala
--- 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)
   }
 }