# HG changeset patch
# User wenzelm
# Date 1274988998 -7200
# Node ID edfbd2a8234f6dd1a3e2af0b96c8c987f563e506
# Parent  d515609c88f794d06ba1b1ee52f968f87a7c311f
slightly odd workaround to ignore markup that is typically displaced;

diff -r d515609c88f7 -r edfbd2a8234f src/Pure/PIDE/state.scala
--- a/src/Pure/PIDE/state.scala	Thu May 27 21:14:53 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Thu May 27 21:36:38 2010 +0200
@@ -99,6 +99,11 @@
                       case _ => state
                     }
                   }
+                  else if (kind == Markup.FACT_DECL || kind == Markup.LOCAL_FACT_DECL ||
+                      kind == Markup.ATTRIBUTE || kind == Markup.FIXED_DECL) {
+                    // FIXME usually displaced due to lack of full history support
+                    state
+                  }
                   else {
                     state.add_markup(
                       command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))