# HG changeset patch
# User wenzelm
# Date 1533064880 -7200
# Node ID 0bc4919387800cc156a2ce02ee5d2577b4b604ea
# Parent  3a02b424d5fb19376a9cf0e04a3c5aedcf0296b2
tuned signature;

diff -r 3a02b424d5fb -r 0bc491938780 src/Pure/Isar/line_structure.scala
--- a/src/Pure/Isar/line_structure.scala	Tue Jul 31 21:11:24 2018 +0200
+++ b/src/Pure/Isar/line_structure.scala	Tue Jul 31 21:21:20 2018 +0200
@@ -23,7 +23,7 @@
 {
   def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure =
   {
-    val improper1 = tokens.forall(_.is_improper)
+    val improper1 = tokens.forall(tok => !tok.is_proper)
     val blank1 = tokens.forall(_.is_space)
     val command1 = tokens.exists(_.is_begin_or_command)
 
diff -r 3a02b424d5fb -r 0bc491938780 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Tue Jul 31 21:11:24 2018 +0200
+++ b/src/Pure/Isar/token.ML	Tue Jul 31 21:21:20 2018 +0200
@@ -43,7 +43,6 @@
   val is_command_modifier: T -> bool
   val ident_with: (string -> bool) -> T -> bool
   val is_proper: T -> bool
-  val is_improper: T -> bool
   val is_comment: T -> bool
   val is_informal_comment: T -> bool
   val is_formal_comment: T -> bool
@@ -236,8 +235,6 @@
   | is_proper (Token (_, (Comment _, _), _)) = false
   | is_proper _ = true;
 
-val is_improper = not o is_proper;
-
 fun is_comment (Token (_, (Comment _, _), _)) = true
   | is_comment _ = false;
 
diff -r 3a02b424d5fb -r 0bc491938780 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Tue Jul 31 21:11:24 2018 +0200
+++ b/src/Pure/Isar/token.scala	Tue Jul 31 21:21:20 2018 +0200
@@ -297,7 +297,6 @@
   def is_formal_comment: Boolean = kind == Token.Kind.FORMAL_COMMENT
   def is_comment: Boolean = is_informal_comment || is_formal_comment
   def is_ignored: Boolean = is_space || is_informal_comment
-  def is_improper: Boolean = is_space || is_comment
   def is_proper: Boolean = !is_space && !is_comment
   def is_error: Boolean = kind == Token.Kind.ERROR
   def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
diff -r 3a02b424d5fb -r 0bc491938780 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Tue Jul 31 21:11:24 2018 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Tue Jul 31 21:21:20 2018 +0200
@@ -26,13 +26,13 @@
     def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
     {
       val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
-      if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
+      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
     }
 
     def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
     {
       val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
-      if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
+      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
     }
   }