diff --git a/ivette/src/dome/renderer/text/editor.tsx b/ivette/src/dome/renderer/text/editor.tsx
index 3426e8b4fa6e2961bf229bf8a7e01b09d2471a25..7ca40b680eba78057fdd0ce13b21e378afbb86b0 100644
--- a/ivette/src/dome/renderer/text/editor.tsx
+++ b/ivette/src/dome/renderer/text/editor.tsx
@@ -24,7 +24,7 @@ import React from 'react';
 
 import { EditorState, StateField, Facet, Extension } from '@codemirror/state';
 import { Annotation, Transaction, RangeSet } from '@codemirror/state';
-import { EditorSelection, Text } from '@codemirror/state';
+import { EditorSelection, Text, Prec } from '@codemirror/state';
 
 import { EditorView, ViewPlugin, ViewUpdate } from '@codemirror/view';
 import { Decoration, DecorationSet } from '@codemirror/view';
@@ -285,6 +285,17 @@ export function createViewUpdater<I extends Dict>(
   return enables.concat(listener);
 }
 
+export type Priority = 'lowest' | 'low' | 'default' | 'high' | 'highest';
+export function setPriority(extension: Extension, p: Priority): Extension {
+  switch(p) {
+    case 'lowest': return Prec.lowest(extension);
+    case 'low': return Prec.low(extension);
+    case 'default': return Prec.default(extension);
+    case 'high': return Prec.high(extension);
+    case 'highest': return Prec.highest(extension);
+  }
+}
+
 // -----------------------------------------------------------------------------
 
 
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index 387b73c1d7cdff90d40b70445ebb7a67544d2e1f..59dfaab846c90896318b96b35ad7a1036f1e06f6 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -274,24 +274,37 @@ function createHoveredUpdater(): Editor.Extension {
 //  Plugin decorating hovered and selected elements
 // -----------------------------------------------------------------------------
 
-const CodeDecorator = createCodeDecorator();
-function createCodeDecorator(): Editor.Extension {
-  const hoveredClass = Editor.Decoration.mark({ class: 'cm-hovered-code' });
-  const selectedClass = Editor.Decoration.mark({ class: 'cm-selected-code' });
-  const multipleClass = Editor.Decoration.mark({ class: 'cm-multiple-code' });
-  const selections = { marker: Marker, multiple: Multiple, hovered: Hovered };
-  const deps = { ranges: Ranges, ...selections };
-  return Editor.createDecorator(deps, (props) => {
-    const { ranges, marker: m, hovered: h, multiple: ms } = props;
+const HoveredDecorator = createHoveredDecorator();
+function createHoveredDecorator(): Editor.Extension {
+  const cls = Editor.Decoration.mark({ class: 'cm-hovered-code' });
+  const deps = { ranges: Ranges, hovered: Hovered };
+  const extension = Editor.createDecorator(deps, ({ ranges, hovered }) => {
+    const hoveredRanges = hovered ? (ranges.get(hovered) ?? []) : [];
+    return Editor.RangeSet.of(hoveredRanges.map(r => cls.range(r.from, r.to)));
+  });
+  return Editor.setPriority(extension, 'highest');
+}
+
+const MarkerDecorator = createMarkerDecorator();
+function createMarkerDecorator(): Editor.Extension {
+  const cls = Editor.Decoration.mark({ class: 'cm-selected-code' });
+  const deps = { ranges: Ranges, marker: Marker };
+  const extension = Editor.createDecorator(deps, ({ ranges, marker }) => {
+    const selectedRanges = marker ? (ranges.get(marker) ?? []) : [];
+    return Editor.RangeSet.of(selectedRanges.map(r => cls.range(r.from, r.to)));
+  });
+  return Editor.setPriority(extension, 'high');
+}
+
+const MultipleDecorator = createMultipleDecorator();
+function createMultipleDecorator(): Editor.Extension {
+  const cls = Editor.Decoration.mark({ class: 'cm-multiple-code' });
+  const deps = { ranges: Ranges, multiple: Multiple };
+  const extension = Editor.createDecorator(deps, ({ ranges, multiple: ms }) => {
     const multRanges = mapFilter(ms.filter(isDef), (m) => ranges.get(m)).flat();
-    const hoveredRanges = h ? (ranges.get(h) ?? []) : [];
-    const selectedRanges = m ? (ranges.get(m) ?? []) : [];
-    const hovered  = hoveredRanges.map(r =>  hoveredClass.range(r.from, r.to));
-    const selected = selectedRanges.map(r => selectedClass.range(r.from, r.to));
-    const multiple = multRanges.map(r => multipleClass.range(r.from, r.to));
-    const decorations = selected.concat(hovered, multiple);
-    return Editor.RangeSet.of(decorations, true);
+    return Editor.RangeSet.of(multRanges.map(r => cls.range(r.from, r.to)));
   });
+  return Editor.setPriority(extension, 'default');
 }
 
 // -----------------------------------------------------------------------------
@@ -620,7 +633,9 @@ const extensions: Editor.Extension[] = [
   MarkerUpdater,
   MarkerScroller,
   HoveredUpdater,
-  CodeDecorator,
+  HoveredDecorator,
+  MarkerDecorator,
+  MultipleDecorator,
   DeadCodeDecorator,
   ContextMenuHandler,
   PropertiesGutter,