clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;

--- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 31 21:06:09 2018 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 31 21:11:24 2018 +0200
@@ -233,7 +233,7 @@
 fun ship span =
   let
     val kind =
-      if forall Token.is_improper span then Command_Span.Ignored_Span
+      if forall Token.is_ignored span then Command_Span.Ignored_Span
       else if exists Token.is_error span then Command_Span.Malformed_Span
       else
         (case find_first Token.is_command span of
@@ -241,18 +241,18 @@
         | SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd));
   in cons (Command_Span.Span (kind, span)) end;
 
-fun flush (result, content, improper) =
+fun flush (result, content, ignored) =
   result
   |> not (null content) ? ship (rev content)
-  |> not (null improper) ? ship (rev improper);
+  |> not (null ignored) ? ship (rev ignored);
 
-fun parse tok (result, content, improper) =
-  if Token.is_improper tok then (result, content, tok :: improper)
+fun parse tok (result, content, ignored) =
+  if Token.is_ignored tok then (result, content, tok :: ignored)
   else if Token.is_command_modifier tok orelse
     Token.is_command tok andalso
       (not (exists Token.is_command_modifier content) orelse exists Token.is_command content)
-  then (flush (result, content, improper), [tok], [])
-  else (result, tok :: (improper @ content), []);
+  then (flush (result, content, ignored), [tok], [])
+  else (result, tok :: (ignored @ content), []);
 
 in
 

--- a/src/Pure/Isar/outer_syntax.scala	Tue Jul 31 21:06:09 2018 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Jul 31 21:11:24 2018 +0200
@@ -161,12 +161,12 @@
   {
     val result = new mutable.ListBuffer[Command_Span.Span]
     val content = new mutable.ListBuffer[Token]
-    val improper = new mutable.ListBuffer[Token]
+    val ignored = new mutable.ListBuffer[Token]
 
     def ship(span: List[Token])
     {
       val kind =
-        if (span.forall(_.is_improper)) Command_Span.Ignored_Span
+        if (span.forall(_.is_ignored)) Command_Span.Ignored_Span
         else if (span.exists(_.is_error)) Command_Span.Malformed_Span
         else
           span.find(_.is_command) match {
@@ -186,16 +186,16 @@
     def flush()
     {
       if (content.nonEmpty) { ship(content.toList); content.clear }
-      if (improper.nonEmpty) { ship(improper.toList); improper.clear }
+      if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear }
     }
 
     for (tok <- toks) {
-      if (tok.is_improper) improper += tok
+      if (tok.is_ignored) ignored += tok
       else if (keywords.is_before_command(tok) ||
         tok.is_command &&
           (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
       { flush(); content += tok }
-      else { content ++= improper; improper.clear; content += tok }
+      else { content ++= ignored; ignored.clear; content += tok }
     }
     flush()
 

--- a/src/Pure/Isar/token.ML	Tue Jul 31 21:06:09 2018 +0200
+++ b/src/Pure/Isar/token.ML	Tue Jul 31 21:11:24 2018 +0200
@@ -47,6 +47,7 @@
   val is_comment: T -> bool
   val is_informal_comment: T -> bool
   val is_formal_comment: T -> bool
+  val is_ignored: T -> bool
   val is_begin_ignore: T -> bool
   val is_end_ignore: T -> bool
   val is_error: T -> bool
@@ -227,6 +228,10 @@
 fun ident_with pred (Token (_, (Ident, x), _)) = pred x
   | ident_with _ _ = false;
 
+fun is_ignored (Token (_, (Space, _), _)) = true
+  | is_ignored (Token (_, (Comment NONE, _), _)) = true
+  | is_ignored _ = false;
+
 fun is_proper (Token (_, (Space, _), _)) = false
   | is_proper (Token (_, (Comment _, _), _)) = false
   | is_proper _ = true;

--- a/src/Pure/Isar/token.scala	Tue Jul 31 21:06:09 2018 +0200
+++ b/src/Pure/Isar/token.scala	Tue Jul 31 21:11:24 2018 +0200
@@ -296,6 +296,7 @@
   def is_informal_comment: Boolean = kind == Token.Kind.INFORMAL_COMMENT
   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

--- a/src/Pure/PIDE/command.ML	Tue Jul 31 21:06:09 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Jul 31 21:11:24 2018 +0200
@@ -136,7 +136,7 @@
   let
     val command_reports = Outer_Syntax.command_reports thy;
 
-    val core_range = Token.range_of (drop_suffix Token.is_improper span);
+    val core_range = Token.range_of (drop_suffix Token.is_ignored span);
     val pos =
       (case find_first Token.is_command span of
         SOME tok => Token.pos_of tok

--- a/src/Pure/PIDE/command.scala	Tue Jul 31 21:06:09 2018 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Jul 31 21:11:24 2018 +0200
@@ -605,7 +605,7 @@
 
   val core_range: Text.Range =
     Text.Range(0,
-      (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
+      (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length))
 
   def source(range: Text.Range): String = range.substring(source)