clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
authorwenzelm
Tue Jul 31 21:11:24 2018 +0200 (9 months ago)
changeset 687293a02b424d5fb
parent 68728 c07f6fa02c59
child 68730 0bc491938780
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/outer_syntax.scala
src/Pure/Isar/token.ML
src/Pure/Isar/token.scala
src/Pure/PIDE/command.ML
src/Pure/PIDE/command.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 31 21:06:09 2018 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 31 21:11:24 2018 +0200
     1.3 @@ -233,7 +233,7 @@
     1.4  fun ship span =
     1.5    let
     1.6      val kind =
     1.7 -      if forall Token.is_improper span then Command_Span.Ignored_Span
     1.8 +      if forall Token.is_ignored span then Command_Span.Ignored_Span
     1.9        else if exists Token.is_error span then Command_Span.Malformed_Span
    1.10        else
    1.11          (case find_first Token.is_command span of
    1.12 @@ -241,18 +241,18 @@
    1.13          | SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd));
    1.14    in cons (Command_Span.Span (kind, span)) end;
    1.15  
    1.16 -fun flush (result, content, improper) =
    1.17 +fun flush (result, content, ignored) =
    1.18    result
    1.19    |> not (null content) ? ship (rev content)
    1.20 -  |> not (null improper) ? ship (rev improper);
    1.21 +  |> not (null ignored) ? ship (rev ignored);
    1.22  
    1.23 -fun parse tok (result, content, improper) =
    1.24 -  if Token.is_improper tok then (result, content, tok :: improper)
    1.25 +fun parse tok (result, content, ignored) =
    1.26 +  if Token.is_ignored tok then (result, content, tok :: ignored)
    1.27    else if Token.is_command_modifier tok orelse
    1.28      Token.is_command tok andalso
    1.29        (not (exists Token.is_command_modifier content) orelse exists Token.is_command content)
    1.30 -  then (flush (result, content, improper), [tok], [])
    1.31 -  else (result, tok :: (improper @ content), []);
    1.32 +  then (flush (result, content, ignored), [tok], [])
    1.33 +  else (result, tok :: (ignored @ content), []);
    1.34  
    1.35  in
    1.36  
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Jul 31 21:06:09 2018 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Jul 31 21:11:24 2018 +0200
     2.3 @@ -161,12 +161,12 @@
     2.4    {
     2.5      val result = new mutable.ListBuffer[Command_Span.Span]
     2.6      val content = new mutable.ListBuffer[Token]
     2.7 -    val improper = new mutable.ListBuffer[Token]
     2.8 +    val ignored = new mutable.ListBuffer[Token]
     2.9  
    2.10      def ship(span: List[Token])
    2.11      {
    2.12        val kind =
    2.13 -        if (span.forall(_.is_improper)) Command_Span.Ignored_Span
    2.14 +        if (span.forall(_.is_ignored)) Command_Span.Ignored_Span
    2.15          else if (span.exists(_.is_error)) Command_Span.Malformed_Span
    2.16          else
    2.17            span.find(_.is_command) match {
    2.18 @@ -186,16 +186,16 @@
    2.19      def flush()
    2.20      {
    2.21        if (content.nonEmpty) { ship(content.toList); content.clear }
    2.22 -      if (improper.nonEmpty) { ship(improper.toList); improper.clear }
    2.23 +      if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear }
    2.24      }
    2.25  
    2.26      for (tok <- toks) {
    2.27 -      if (tok.is_improper) improper += tok
    2.28 +      if (tok.is_ignored) ignored += tok
    2.29        else if (keywords.is_before_command(tok) ||
    2.30          tok.is_command &&
    2.31            (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
    2.32        { flush(); content += tok }
    2.33 -      else { content ++= improper; improper.clear; content += tok }
    2.34 +      else { content ++= ignored; ignored.clear; content += tok }
    2.35      }
    2.36      flush()
    2.37  
     3.1 --- a/src/Pure/Isar/token.ML	Tue Jul 31 21:06:09 2018 +0200
     3.2 +++ b/src/Pure/Isar/token.ML	Tue Jul 31 21:11:24 2018 +0200
     3.3 @@ -47,6 +47,7 @@
     3.4    val is_comment: T -> bool
     3.5    val is_informal_comment: T -> bool
     3.6    val is_formal_comment: T -> bool
     3.7 +  val is_ignored: T -> bool
     3.8    val is_begin_ignore: T -> bool
     3.9    val is_end_ignore: T -> bool
    3.10    val is_error: T -> bool
    3.11 @@ -227,6 +228,10 @@
    3.12  fun ident_with pred (Token (_, (Ident, x), _)) = pred x
    3.13    | ident_with _ _ = false;
    3.14  
    3.15 +fun is_ignored (Token (_, (Space, _), _)) = true
    3.16 +  | is_ignored (Token (_, (Comment NONE, _), _)) = true
    3.17 +  | is_ignored _ = false;
    3.18 +
    3.19  fun is_proper (Token (_, (Space, _), _)) = false
    3.20    | is_proper (Token (_, (Comment _, _), _)) = false
    3.21    | is_proper _ = true;
     4.1 --- a/src/Pure/Isar/token.scala	Tue Jul 31 21:06:09 2018 +0200
     4.2 +++ b/src/Pure/Isar/token.scala	Tue Jul 31 21:11:24 2018 +0200
     4.3 @@ -296,6 +296,7 @@
     4.4    def is_informal_comment: Boolean = kind == Token.Kind.INFORMAL_COMMENT
     4.5    def is_formal_comment: Boolean = kind == Token.Kind.FORMAL_COMMENT
     4.6    def is_comment: Boolean = is_informal_comment || is_formal_comment
     4.7 +  def is_ignored: Boolean = is_space || is_informal_comment
     4.8    def is_improper: Boolean = is_space || is_comment
     4.9    def is_proper: Boolean = !is_space && !is_comment
    4.10    def is_error: Boolean = kind == Token.Kind.ERROR
     5.1 --- a/src/Pure/PIDE/command.ML	Tue Jul 31 21:06:09 2018 +0200
     5.2 +++ b/src/Pure/PIDE/command.ML	Tue Jul 31 21:11:24 2018 +0200
     5.3 @@ -136,7 +136,7 @@
     5.4    let
     5.5      val command_reports = Outer_Syntax.command_reports thy;
     5.6  
     5.7 -    val core_range = Token.range_of (drop_suffix Token.is_improper span);
     5.8 +    val core_range = Token.range_of (drop_suffix Token.is_ignored span);
     5.9      val pos =
    5.10        (case find_first Token.is_command span of
    5.11          SOME tok => Token.pos_of tok
     6.1 --- a/src/Pure/PIDE/command.scala	Tue Jul 31 21:06:09 2018 +0200
     6.2 +++ b/src/Pure/PIDE/command.scala	Tue Jul 31 21:11:24 2018 +0200
     6.3 @@ -605,7 +605,7 @@
     6.4  
     6.5    val core_range: Text.Range =
     6.6      Text.Range(0,
     6.7 -      (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
     6.8 +      (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
     6.9  
    6.10    def source(range: Text.Range): String = range.substring(source)
    6.11