From 8da3108378dd0df0df2e0302e6c54c08f05a0935 Mon Sep 17 00:00:00 2001 From: Namyl Date: Thu, 5 Mar 2026 19:25:17 +0100 Subject: [PATCH 1/2] Node marking in proof tree and code syntax highlighting --- src/lib/components/ProofTree.svelte | 40 +++++++++++++- src/lib/components/TermTree.svelte | 85 +++++++++++++++++++++++++++++ 2 files changed, 124 insertions(+), 1 deletion(-) 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} {:else} -
{item.label}
+
{item.label}
{/if} {/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..bd8692b 100644 --- a/src/lib/components/TermTree.svelte +++ b/src/lib/components/TermTree.svelte @@ -171,6 +171,78 @@ // TODO: Post error to error widget. }); } + + // --- Rust syntax highlighting --- + + const RUST_KEYWORDS = new Set([ + "as", "async", "await", "break", "const", "continue", "crate", "dyn", + "else", "enum", "extern", "false", "fn", "for", "if", "impl", "in", + "let", "loop", "match", "mod", "move", "mut", "pub", "ref", "return", + "self", "Self", "static", "struct", "super", "trait", "true", "type", + "unsafe", "use", "where", "while", + ]); + + const RUST_TYPES = new Set([ + "i8", "i16", "i32", "i64", "i128", "isize", + "u8", "u16", "u32", "u64", "u128", "usize", + "f32", "f64", "bool", "char", "str", "String", + "Vec", "Option", "Result", "Box", "Rc", "Arc", + "HashMap", "HashSet", "BTreeMap", "BTreeSet", + "Cell", "RefCell", "Mutex", "RwLock", + ]); + + type RustTokenKind = + | "keyword" + | "type" + | "number" + | "string" + | "comment" + | "lifetime" + | "macro" + | "operator" + | "punctuation" + | "plain"; + + function rustTokenKind(token: string): RustTokenKind { + const t = token.trim(); + if (t === "") return "plain"; + + // Line comment + if (t.startsWith("//")) return "comment"; + + // String / char literal + if ( + (t.startsWith('"') && t.endsWith('"')) || + (t.startsWith("'") && t.endsWith("'") && t.length > 2) || + (t.startsWith('b"') && t.endsWith('"')) || + t.startsWith('r#"') + ) return "string"; + + // Lifetime e.g. 'a 'static + if (/^'[a-z_][a-z0-9_]*$/.test(t)) return "lifetime"; + + // Macro call e.g. println! + if (/^[a-z_][a-z0-9_]*!$/.test(t)) return "macro"; + + // Keywords + if (RUST_KEYWORDS.has(t)) return "keyword"; + + // Built-in types + if (RUST_TYPES.has(t)) return "type"; + + // Numbers: integer, float, hex, binary, octal with optional suffix + if (/^-?(?:0x[0-9a-fA-F_]+|0b[01_]+|0o[0-7_]+|[0-9][0-9_]*(?:\.[0-9_]+)?(?:[eE][+-]?[0-9_]+)?)(?:_?(?:i8|i16|i32|i64|i128|isize|u8|u16|u32|u64|u128|usize|f32|f64))?$/.test(t)) + return "number"; + + // Operators + if (/^(?:=>|->|::|\.\.=|\.\.|\+=|-=|\*=|\/=|%=|&&|\|\||[+\-*/%&|^!<>=?@~]+)$/.test(t)) + return "operator"; + + // Punctuation + if (/^[{}()[\];:,.]$/.test(t)) return "punctuation"; + + return "plain"; + }
@@ -180,6 +252,7 @@ onmouseout={(e) => onMouseOut(index)} onclick={(e) => onClick(e, index)} class:span-hover={isMarked(index)} + class="rust-{rustTokenKind(span.content)}" > {span.content} @@ -231,6 +304,18 @@ background-color: gray; } + /* Rust syntax highlighting */ + .rust-keyword { color: #cc99cd; font-weight: 600; } + .rust-type { color: #4ec9b0; } + .rust-number { color: #b5cea8; } + .rust-string { color: #ce9178; } + .rust-comment { color: #6a9955; font-style: italic; } + .rust-lifetime { color: #d7ba7d; } + .rust-macro { color: #dcdcaa; } + .rust-operator { color: #d4d4d4; } + .rust-punctuation { color: #808080; } + .rust-plain { color: inherit; } + .ctx-menu { position: absolute; background: #1f1f1f; From 732ccb6e3f298405e66b67a2441b5bd0a2f429aa Mon Sep 17 00:00:00 2001 From: Namyl Date: Thu, 5 Mar 2026 22:40:05 +0100 Subject: [PATCH 2/2] updated sequent highlighting for rust --- src/lib/components/TermTree.svelte | 230 +++++++++++------------------ 1 file changed, 89 insertions(+), 141 deletions(-) diff --git a/src/lib/components/TermTree.svelte b/src/lib/components/TermTree.svelte index bd8692b..c809c66 100644 --- a/src/lib/components/TermTree.svelte +++ b/src/lib/components/TermTree.svelte @@ -1,19 +1,15 @@ @@ -252,7 +215,7 @@ onmouseout={(e) => onMouseOut(index)} onclick={(e) => onClick(e, index)} class:span-hover={isMarked(index)} - class="rust-{rustTokenKind(span.content)}" + class={hljsClassForSpan(span)} > {span.content} @@ -263,23 +226,15 @@ class="ctx-menu" style="top: {contextMenuState.y}px; left: {contextMenuState.x}px;" > -
- applyAction(action.commandId)} - /> - applyAction(action.commandId)} - /> - applyAction(action.commandId)} - /> -
+
    + {#each contextMenuState.actions as action} +
  • + +
    • + {/each} +
{/if} @@ -304,17 +259,9 @@ background-color: gray; } - /* Rust syntax highlighting */ - .rust-keyword { color: #cc99cd; font-weight: 600; } - .rust-type { color: #4ec9b0; } - .rust-number { color: #b5cea8; } - .rust-string { color: #ce9178; } - .rust-comment { color: #6a9955; font-style: italic; } - .rust-lifetime { color: #d7ba7d; } - .rust-macro { color: #dcdcaa; } - .rust-operator { color: #d4d4d4; } - .rust-punctuation { color: #808080; } - .rust-plain { color: inherit; } + .span-hover { + background-color: gray; + } .ctx-menu { position: absolute; @@ -326,8 +273,9 @@ z-index: 1000; } - .action-list { - display: flex; - overflow: scroll; + .ctx-menu ul { + list-style-type: none; + padding: 0; + margin: 0; }