more information;
authorwenzelm
Fri, 23 Jun 2017 14:59:00 +0200
changeset 66177 7fd83f20e3e9
parent 66176 b51a40281016
child 66178 5f02bf37324f
more information;
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)
   }
 }