# HG changeset patch
# User wenzelm
# Date 1397133389 -7200
# Node ID db929027e70131457e65cbbefdf2b77d5d2c211e
# Parent  34ea4d7f236c52079e70a3ceaad7363dfe7864ff
ignore other_id reports for now (see 8eda56033203): massive amounts of redirections to 'class' etc. makes it difficult to edit main HOL;
silently ignore excessive reports -- no ambition to detect that situation accurately;

diff -r 34ea4d7f236c -r db929027e701 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Apr 10 14:27:35 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Apr 10 14:36:29 2014 +0200
@@ -207,11 +207,7 @@
                         case None => bad(); state
                       }
                     case None =>
-                      chunk_name match {
-                        // FIXME workaround for static positions stemming from batch build
-                        case Text.Chunk.File(name) if name.endsWith(".thy") =>
-                        case _ => bad()
-                      }
+                      // silently ignore excessive reports
                       state
                   }
 
diff -r 34ea4d7f236c -r db929027e701 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Apr 10 14:27:35 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Apr 10 14:36:29 2014 +0200
@@ -536,9 +536,11 @@
       id == st.command.id ||
       (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
 
-    private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] =
+    private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] = None
+    /* FIXME
       (execs.get(id) orElse commands.get(id)).map(st =>
         ((Text.Chunk.Id(st.command.id), st.command.chunk)))
+    */
 
     private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
       (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>