src/Pure/Isar/outer_syntax.scala
changeset 68729 3a02b424d5fb
parent 67005 11fca474d87a
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Jul 31 21:06:09 2018 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Jul 31 21:11:24 2018 +0200
     1.3 @@ -161,12 +161,12 @@
     1.4    {
     1.5      val result = new mutable.ListBuffer[Command_Span.Span]
     1.6      val content = new mutable.ListBuffer[Token]
     1.7 -    val improper = new mutable.ListBuffer[Token]
     1.8 +    val ignored = new mutable.ListBuffer[Token]
     1.9  
    1.10      def ship(span: List[Token])
    1.11      {
    1.12        val kind =
    1.13 -        if (span.forall(_.is_improper)) Command_Span.Ignored_Span
    1.14 +        if (span.forall(_.is_ignored)) Command_Span.Ignored_Span
    1.15          else if (span.exists(_.is_error)) Command_Span.Malformed_Span
    1.16          else
    1.17            span.find(_.is_command) match {
    1.18 @@ -186,16 +186,16 @@
    1.19      def flush()
    1.20      {
    1.21        if (content.nonEmpty) { ship(content.toList); content.clear }
    1.22 -      if (improper.nonEmpty) { ship(improper.toList); improper.clear }
    1.23 +      if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear }
    1.24      }
    1.25  
    1.26      for (tok <- toks) {
    1.27 -      if (tok.is_improper) improper += tok
    1.28 +      if (tok.is_ignored) ignored += tok
    1.29        else if (keywords.is_before_command(tok) ||
    1.30          tok.is_command &&
    1.31            (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
    1.32        { flush(); content += tok }
    1.33 -      else { content ++= improper; improper.clear; content += tok }
    1.34 +      else { content ++= ignored; ignored.clear; content += tok }
    1.35      }
    1.36      flush()
    1.37