diff --git a/src/lib/components/ProofTree.svelte b/src/lib/components/ProofTree.svelte
index 667d54f..87fc6f3 100644
--- a/src/lib/components/ProofTree.svelte
+++ b/src/lib/components/ProofTree.svelte
@@ -141,6 +141,28 @@
         return "unknown";
     }
 
+    // Returns the status of a virtual node's branch based on its descendants
+    function virtualStatus(index: number): "open" | "closed" | "mixed" {
+        let hasOpen = false;
+        let hasClosed = false;
+        const currentDepth = nodes[index]?.depth ?? 0;
+
+        for (let i = index + 1; i < nodes.length; i++) {
+            const item = nodes[i];
+            if (item.depth <= currentDepth) break;
+            if (item.kind !== "real") continue;
+
+            const s = statusFromName(item.node.name);
+            if (s === "open") hasOpen = true;
+            if (s === "closed") hasClosed = true;
+            if (hasOpen && hasClosed) return "mixed";
+        }
+
+        if (hasOpen) return "open";
+        if (hasClosed) return "closed";
+        return "open"; // fallback: treat unknown as open
+    }
+
     function isLeaf(index: number) {
         const currentDepth = nodes[index]?.depth ?? 0;
         const nextDepth = nodes[index + 1]?.depth ?? -1;
@@ -362,7 +384,7 @@
                             {Number(item.node.id.nodeId)}: {item.node.name}
                         </button>
                     {:else}
-                        <div class="virtual">{item.label}</div>
+                        <div class="virtual {virtualStatus(index)}">{item.label}</div>
                     {/if}
                 </li>
             {/if}
@@ -540,6 +562,22 @@
         background: rgba(255, 255, 255, 0.04);
         font-weight: 600;
     }
+    
+    .virtual.open {
+        border-color: rgba(255, 100, 100, 0.45);
+        background: rgba(255, 80, 80, 0.1);
+    }
+
+    .virtual.closed {
+        border-color: rgba(80, 200, 120, 0.45);
+        background: rgba(80, 200, 120, 0.1);
+    }
+
+    .virtual.mixed {
+        border-color: rgba(255, 180, 60, 0.45);
+        background: rgba(255, 180, 60, 0.08);
+    }
+
 
     .collapse-icon {
         display: inline-flex;
diff --git a/src/lib/components/TermTree.svelte b/src/lib/components/TermTree.svelte
index fcd1877..c809c66 100644
--- a/src/lib/components/TermTree.svelte
+++ b/src/lib/components/TermTree.svelte
@@ -1,19 +1,15 @@
 <script lang="ts">
-    import { asClassComponent } from "svelte/legacy";
-    import {
-        type TermActionDesc,
-        type NodeTextSpan,
-        type TermActionId,
-        TermActionKind,
+    import type {
+        TermActionDesc,
+        NodeTextSpan,
+        TermActionId,
     } from "../../routes/api";
-    import RuleList from "./sequent/RuleList.svelte";
 
     let { appState, sequent } = $props();
 
     type Span = {
         content: string;
         // All span indices that are associated with this span.
-        // This includes all children.
         // These should be marked when the span is hovered.
         spans: number[];
         // The character index where the text for this span starts.
@@ -79,7 +75,7 @@
         return output;
     }
 
-    const spans = expandTerms(sequent.result, sequent.terms, 0, 0);
+    let spans = expandTerms(sequent.result, sequent.terms, 0, 0);
     let hoveredElement = $state<number | null>(null);
 
     function onMouseOver(index: number) {
@@ -100,28 +96,18 @@
         return spans[hoveredElement].spans.includes(index);
     }
 
-    type Actions = {
-        taclets: TermActionDesc[];
-        macros: TermActionDesc[];
-        other: TermActionDesc[];
-    };
-
     type ContextMenuState = {
         open: boolean;
         x: number;
         y: number;
-        actions: Actions;
+        actions: TermActionDesc[];
     };
 
     let contextMenuState = $state<ContextMenuState>({
-        open: false,
+        open: true,
         x: 0,
         y: 0,
-        actions: {
-            taclets: [],
-            macros: [],
-            other: [],
-        },
+        actions: [],
     });
 
     function onClick(event: MouseEvent, index: number) {
@@ -130,27 +116,11 @@
         appState.client
             .goalActions(sequent.id, textStart)
             .then((actions: TermActionDesc[]) => {
-                const taclets = actions.filter(
-                    (a) => a.kind === TermActionKind.Taclet,
-                );
-                const macros = actions.filter(
-                    (a) => a.kind === TermActionKind.Macro,
-                );
-                const other = actions.filter(
-                    (a) =>
-                        a.kind != TermActionKind.Taclet &&
-                        a.kind != TermActionKind.Macro,
-                );
-
                 contextMenuState = {
                     open: true,
                     x: event.pageX,
                     y: event.pageY,
-                    actions: {
-                        taclets,
-                        macros,
-                        other,
-                    },
+                    actions,
                 };
             });
     }
@@ -171,6 +141,71 @@
                 // TODO: Post error to error widget.
             });
     }
+
+    import hljs from "highlight.js";
+    import "highlight.js/styles/github-dark.css";
+
+    // Build a char-position → hljs class lookup from hljs HTML output.
+    // hljs.highlight() returns HTML like:
+    //   <span class="hljs-keyword">if</span> b <span class="hljs-number">3u32</span>
+    // We strip the tags and record which class was active at each char index.
+    function buildHljsColorMap(text: string, language: string): string[] {
+        const result = hljs.highlight(text, { language, ignoreIllegals: true });
+        const html = result.value;
+
+        const colorMap: string[] = new Array(text.length).fill("");
+        let charPos = 0;
+        let currentClass = "";
+
+        // Simple HTML parser — walks through the hljs output char by char.
+        let i = 0;
+        while (i < html.length) {
+            if (html[i] === "<") {
+                const tagEnd = html.indexOf(">", i);
+                if (tagEnd === -1) break;
+                const tag = html.slice(i + 1, tagEnd);
+
+                if (tag.startsWith("/span")) {
+                    currentClass = "";
+                } else if (tag.startsWith("span")) {
+                    // Extract class name from e.g. 'span class="hljs-keyword"'
+                    const m = tag.match(/class="([^"]+)"/);
+                    currentClass = m ? m[1] : "";
+                }
+                i = tagEnd + 1;
+            } else {
+                // Decode basic HTML entities that hljs emits
+                let ch: string;
+                if (html.startsWith("&amp;", i))  { ch = "&";  i += 5; }
+                else if (html.startsWith("&lt;", i))   { ch = "<";  i += 4; }
+                else if (html.startsWith("&gt;", i))   { ch = ">";  i += 4; }
+                else if (html.startsWith("&quot;", i)) { ch = '"';  i += 6; }
+                else                                    { ch = html[i]; i += 1; }
+
+                if (charPos < colorMap.length) {
+                    colorMap[charPos] = currentClass;
+                    charPos++;
+                }
+            }
+        }
+
+        return colorMap;
+    }
+
+    const hljsColorMap = buildHljsColorMap(sequent.result, "rust");
+
+    // Returns the hljs class for a given span based on its textStart position.
+    // Uses the first non-whitespace character of the span for best accuracy.
+    function hljsClassForSpan(span: Span): string {
+        const text = span.content;
+        for (let i = 0; i < text.length; i++) {
+            if (text[i].trim() !== "") {
+                const pos = span.textStart + i;
+                return hljsColorMap[pos] ?? "";
+            }
+        }
+        return "";
+    }
 </script>
 
 <div class="tree">
@@ -180,6 +215,7 @@
             onmouseout={(e) => onMouseOut(index)}
             onclick={(e) => onClick(e, index)}
             class:span-hover={isMarked(index)}
+            class={hljsClassForSpan(span)}
         >
             {span.content}
         </span>
@@ -190,23 +226,15 @@
             class="ctx-menu"
             style="top: {contextMenuState.y}px; left: {contextMenuState.x}px;"
         >
-            <div class="action-list">
-                <RuleList
-                    name={"Taclet"}
-                    actions={contextMenuState.actions.taclets}
-                    onApply={(action) => applyAction(action.commandId)}
-                />
-                <RuleList
-                    name={"Macros"}
-                    actions={contextMenuState.actions.macros}
-                    onApply={(action) => applyAction(action.commandId)}
-                />
-                <RuleList
-                    name={"Other"}
-                    actions={contextMenuState.actions.other}
-                    onApply={(action) => applyAction(action.commandId)}
-                />
-            </div>
+            <ul>
+                {#each contextMenuState.actions as action}
+                    <li>
+                        <button onclick={() => applyAction(action.commandId)}
+                            >{action.displayName}</button
+                        >
+                    </li>
+                {/each}
+            </ul>
         </div>
     {/if}
 </div>
@@ -231,6 +259,10 @@
         background-color: gray;
     }
 
+    .span-hover {
+        background-color: gray;
+    }
+
     .ctx-menu {
         position: absolute;
         background: #1f1f1f;
@@ -241,8 +273,9 @@
         z-index: 1000;
     }
 
-    .action-list {
-        display: flex;
-        overflow: scroll;
+    .ctx-menu ul {
+        list-style-type: none;
+        padding: 0;
+        margin: 0;
     }
 </style>