# HG changeset patch
# User wenzelm
# Date 1477597932 -7200
# Node ID 681fae6b00b5e118388ae4dc995a93401ece0190
# Parent  2efc128370fa8ece6245d8bc1ddb09bca30d30d6
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;

diff -r 2efc128370fa -r 681fae6b00b5 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Oct 27 20:41:06 2016 +0200
+++ b/src/Pure/Isar/token.ML	Thu Oct 27 21:52:12 2016 +0200
@@ -507,8 +507,9 @@
       SOME {name, ...} => (src, Name_Space.get table name)
     | NONE =>
         let
-          val (name, x) =
-            Name_Space.check (Context.Proof ctxt) table (content_of head, pos_of head);
+          val pos = pos_of head;
+          val (name, x) = Name_Space.check (Context.Proof ctxt) table (content_of head, pos);
+          val _ = Context_Position.report ctxt pos Markup.operator;
           val kind = Name_Space.kind_of (Name_Space.space_of_table table);
           fun print ctxt' =
             Name_Space.markup_extern ctxt' (Name_Space.space_of_table (get_table ctxt')) name;
@@ -720,11 +721,15 @@
 fun syntax_generic scan src context =
   let
     val (name, pos) = name_of_src src;
+    val old_reports = maps reports_of_value src;
     val args1 = map init_assignable (args_of_src src);
     fun reported_text () =
       if Context_Position.is_visible_generic context then
-        ((pos, Markup.operator) :: maps (reports_of_value o closure) args1)
-        |> map (fn (p, m) => Position.reported_text p m "")
+        let val new_reports = maps (reports_of_value o closure) args1 in
+          if old_reports <> new_reports then
+            map (fn (p, m) => Position.reported_text p m "") new_reports
+          else []
+        end
       else [];
   in
     (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of