1.1 --- a/src/Pure/PIDE/state.scala	Thu May 27 21:14:53 2010 +0200
     1.2 +++ b/src/Pure/PIDE/state.scala	Thu May 27 21:36:38 2010 +0200
     1.3 @@ -99,6 +99,11 @@
     1.4                        case _ => state
     1.5                      }
     1.6                    }
     1.7 +                  else if (kind == Markup.FACT_DECL || kind == Markup.LOCAL_FACT_DECL ||
     1.8 +                      kind == Markup.ATTRIBUTE || kind == Markup.FIXED_DECL) {
     1.9 +                    // FIXME usually displaced due to lack of full history support
    1.10 +                    state
    1.11 +                  }
    1.12                    else {
    1.13                      state.add_markup(
    1.14                        command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))