slightly odd workaround to ignore markup that is typically displaced;
authorwenzelm
Thu, 27 May 2010 21:36:38 +0200
changeset 37149 edfbd2a8234f
parent 37148 d515609c88f7
child 37158 c96e119b7fe9
slightly odd workaround to ignore markup that is typically displaced;
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)))