diff --git a/ivette/src/dome/renderer/text/richtext.tsx b/ivette/src/dome/renderer/text/richtext.tsx
index c6d0293ffc27b7a8b715d20cc4932a579cd41227..03859f53447d43b877d70910a16cf0b431fbf111 100644
--- a/ivette/src/dome/renderer/text/richtext.tsx
+++ b/ivette/src/dome/renderer/text/richtext.tsx
@@ -114,7 +114,8 @@ class DiffBuffer {
 function updateContents(view: CM.EditorView, newText: string): void {
   const buffer = new DiffBuffer();
   diffLines(view.state.doc.toString(), newText).forEach(buffer.add);
-  view.dispatch({ changes: buffer.flush() });
+  const changes = buffer.flush();
+  view.dispatch({ changes });
 }
 
 /* -------------------------------------------------------------------------- */
@@ -814,19 +815,6 @@ interface Decorator {
   gutters : CS.RangeSet<CM.GutterMarker>;
 }
 
-function compareDecorations(a : Decorations, b : Decorations): boolean
-{
-  if (a === b) return true;
-  if (!a || isDecoration(a)) return false;
-  if (!b || isDecoration(b)) return false;
-  const n = a.length;
-  if (n !== b.length) return false;
-  for (let k = 0; k < n; k++)
-    if (!compareDecorations(a[k], b[k]))
-      return false;
-  return true;
-}
-
 const DecoratorSpec = CS.Annotation.define<Decorations>();
 
 const DecoratorState = CS.StateField.define<Decorator>({
@@ -839,7 +827,7 @@ const DecoratorState = CS.StateField.define<Decorator>({
 
   update(value: Decorator, tr: CS.Transaction) {
     const newSpec : Decorations = tr.annotation(DecoratorSpec) ?? null;
-    if (newSpec !== null && !compareDecorations(newSpec, value.spec)) {
+    if (newSpec !== null) {
       const builder = new DecorationsBuilder(tr.newDoc);
       builder.addSpec(newSpec);
       return {
diff --git a/ivette/src/frama-c/plugins/wp/style.css b/ivette/src/frama-c/plugins/wp/style.css
index d396e4c9c4a9affa4eed1bc221ebffa852e509ca..eab44e5565f0e23534e141a1f2eb3d820a7ae515 100644
--- a/ivette/src/frama-c/plugins/wp/style.css
+++ b/ivette/src/frama-c/plugins/wp/style.css
@@ -2,6 +2,14 @@
 /* --- WP Panel Styles                                                    --- */
 /* -------------------------------------------------------------------------- */
 
+.wp .cm-gutter {
+    width: 3px;
+}
+
+.wp-gutter-part {
+    background: red;
+}
+
 .wp.cm-hovered-code,
 .wp.cm-hovered-code > span
 {
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
index dc4e100710bc9a63b5fbfd756adec83dcbe74b6f..586ea2c5f9889abd3bc1bc9d07206076b447ac6f 100644
--- a/ivette/src/frama-c/plugins/wp/tip.tsx
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -28,8 +28,8 @@ import { Cell } from 'dome/controls/labels';
 import { ToolBar, Select, Filler } from 'dome/frame/toolbars';
 import { Vfill } from 'dome/layout/boxes';
 import {
-  MarkDecoration, Decorations,
-  Position, TextView
+  MarkDecoration, GutterDecoration, Decorations,
+  Position, Range, TextProxy, TextView,
 } from 'dome/text/richtext';
 
 import * as Server from 'frama-c/server';
@@ -116,6 +116,7 @@ function RFormatSelector(props: Selector<TIP.rformat>): JSX.Element {
 
 type Node = TIP.node | undefined;
 type Location = { part?: RichText.Tag, term?: RichText.Tag };
+type Target = { selection?: Range, gutters: GutterDecoration[] };
 
 class Sequent {
   private readonly contents: string;
@@ -185,6 +186,20 @@ class Sequent {
     return ptags[0];
   }
 
+  target(proxy: TextProxy, part?: TIP.part, term?: TIP.term): Target {
+    const tag = this.select(part, term);
+    const gutters: GutterDecoration[] = [];
+    if (tag) {
+      const selection: Range = { offset: tag.offset, length: 0 };
+      const lineFrom = proxy.lineAt(tag.offset+1);
+      const lineTo = proxy.lineAt(tag.endOffset);
+      for (let line = lineFrom; line <= lineTo; line++)
+        gutters.push({ className: 'wp-gutter-part', gutter: '|', line });
+      return { selection, gutters };
+    } else
+      return { selection: undefined, gutters };
+  }
+
   locate(position: number): Location {
     const isPart = ({ tag }: RichText.Tag): boolean => {
       return tag === '#goal' || tag.startsWith('#s');
@@ -227,16 +242,18 @@ function GoalView(props: GoalViewProps): JSX.Element {
   const unmangled = focus === 'MEMORY' || focus === 'RAW';
   const jtext = States.useRequest(TIP.printSequent, {
     node, iformat, rformat, autofocus, unmangled,
+  }, {
+    pending: null,
+    offline: undefined,
+    onError: '',
   }) ?? null;
   const { part, term } = States.useRequest(TIP.getSelection, node) ?? {};
+  const proxy = React.useMemo(() => new TextProxy(), []);
   const sequent = React.useMemo(() => new Sequent(jtext), [jtext]);
-  const selection = React.useMemo(
-    () => {
-      const tag = sequent.select(part, term);
-      const selection = tag && { offset: tag.offset, length: 0 };
-      return selection;
-    },
-    [sequent, part, term]
+  React.useEffect(() => proxy.updateContents(sequent.text), [proxy, sequent]);
+  const { selection, gutters } = React.useMemo(
+    () => sequent.target(proxy, part, term),
+    [sequent, proxy, part, term]
   );
   const [hover, setHover] = React.useState<Decorations>(null);
   const onHover = React.useCallback((pos: Position | null) => {
@@ -244,15 +261,13 @@ function GoalView(props: GoalViewProps): JSX.Element {
   }, [sequent]);
   const onClick = React.useCallback((pos: Position | null) => {
     setHover(null);
-    if (node) {
-      if (pos) {
-        const loc = sequent.locate(pos.offset);
-        const part = jOption(TIP.jPart)(loc.part?.tag);
-        const term = jOption(TIP.jTerm)(loc.term?.tag);
-        if (part || term) {
-          Server.send(TIP.setSelection, { node, part, term });
-          return;
-        }
+    if (node && pos) {
+      const loc = sequent.locate(pos.offset);
+      const part = jOption(TIP.jPart)(loc.part?.tag);
+      const term = jOption(TIP.jTerm)(loc.term?.tag);
+      if (part || term) {
+        Server.send(TIP.setSelection, { node, part, term });
+        return;
       }
     }
     Server.send(TIP.clearSelection, node);
@@ -260,9 +275,10 @@ function GoalView(props: GoalViewProps): JSX.Element {
   return (
     <TextView
       readOnly
-      text={sequent.text}
+      className='wp'
+      text={proxy}
       selection={selection}
-      decorations={[hover, sequent.decorations]}
+      decorations={[hover, sequent.decorations, gutters]}
       onHover={onHover}
       onClick={onClick}
     />