tuned signature;
authorwenzelm
Tue Jul 31 21:21:20 2018 +0200 (9 months ago)
changeset 687300bc491938780
parent 68729 3a02b424d5fb
child 68731 c2dcb7f7a3ef
tuned signature;
src/Pure/Isar/line_structure.scala
src/Pure/Isar/token.ML
src/Pure/Isar/token.scala
src/Tools/jEdit/src/text_structure.scala
     1.1 --- a/src/Pure/Isar/line_structure.scala	Tue Jul 31 21:11:24 2018 +0200
     1.2 +++ b/src/Pure/Isar/line_structure.scala	Tue Jul 31 21:21:20 2018 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  {
     1.5    def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure =
     1.6    {
     1.7 -    val improper1 = tokens.forall(_.is_improper)
     1.8 +    val improper1 = tokens.forall(tok => !tok.is_proper)
     1.9      val blank1 = tokens.forall(_.is_space)
    1.10      val command1 = tokens.exists(_.is_begin_or_command)
    1.11  
     2.1 --- a/src/Pure/Isar/token.ML	Tue Jul 31 21:11:24 2018 +0200
     2.2 +++ b/src/Pure/Isar/token.ML	Tue Jul 31 21:21:20 2018 +0200
     2.3 @@ -43,7 +43,6 @@
     2.4    val is_command_modifier: T -> bool
     2.5    val ident_with: (string -> bool) -> T -> bool
     2.6    val is_proper: T -> bool
     2.7 -  val is_improper: T -> bool
     2.8    val is_comment: T -> bool
     2.9    val is_informal_comment: T -> bool
    2.10    val is_formal_comment: T -> bool
    2.11 @@ -236,8 +235,6 @@
    2.12    | is_proper (Token (_, (Comment _, _), _)) = false
    2.13    | is_proper _ = true;
    2.14  
    2.15 -val is_improper = not o is_proper;
    2.16 -
    2.17  fun is_comment (Token (_, (Comment _, _), _)) = true
    2.18    | is_comment _ = false;
    2.19  
     3.1 --- a/src/Pure/Isar/token.scala	Tue Jul 31 21:11:24 2018 +0200
     3.2 +++ b/src/Pure/Isar/token.scala	Tue Jul 31 21:21:20 2018 +0200
     3.3 @@ -297,7 +297,6 @@
     3.4    def is_formal_comment: Boolean = kind == Token.Kind.FORMAL_COMMENT
     3.5    def is_comment: Boolean = is_informal_comment || is_formal_comment
     3.6    def is_ignored: Boolean = is_space || is_informal_comment
     3.7 -  def is_improper: Boolean = is_space || is_comment
     3.8    def is_proper: Boolean = !is_space && !is_comment
     3.9    def is_error: Boolean = kind == Token.Kind.ERROR
    3.10    def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
     4.1 --- a/src/Tools/jEdit/src/text_structure.scala	Tue Jul 31 21:11:24 2018 +0200
     4.2 +++ b/src/Tools/jEdit/src/text_structure.scala	Tue Jul 31 21:21:20 2018 +0200
     4.3 @@ -26,13 +26,13 @@
     4.4      def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
     4.5      {
     4.6        val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
     4.7 -      if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
     4.8 +      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
     4.9      }
    4.10  
    4.11      def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    4.12      {
    4.13        val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
    4.14 -      if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
    4.15 +      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
    4.16      }
    4.17    }
    4.18