# 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) } }