author | wenzelm |
Thu, 27 May 2010 21:36:38 +0200 | |
changeset 37149 | edfbd2a8234f |
parent 37148 | d515609c88f7 |
child 37158 | c96e119b7fe9 |
--- 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)))