From 9a26f6dab59f42c23d710bc7d08d13b19d9ba31c Mon Sep 17 00:00:00 2001 From: RanimZayen Date: Wed, 28 Jan 2026 22:52:00 +0100 Subject: [PATCH 1/2] Taclet info display in proof tree --- src/lib/components/ProofTree.svelte | 209 +++++++++++++++++++++++----- src/routes/+page.svelte | 5 +- src/routes/api.ts | 7 + 3 files changed, 182 insertions(+), 39 deletions(-) diff --git a/src/lib/components/ProofTree.svelte b/src/lib/components/ProofTree.svelte index c7fd478..5503e5d 100644 --- a/src/lib/components/ProofTree.svelte +++ b/src/lib/components/ProofTree.svelte @@ -10,11 +10,15 @@ let nodes = $state([]); + //State for the context menu type CtxMenuState = { open: boolean; x: number; y: number; node: TreeNodeDesc | null; + appliedOn: string | null; + loading: boolean; + error: string | null; }; let ctxMenu = $state({ @@ -22,16 +26,74 @@ x: 0, y: 0, node: null, + appliedOn: null, + loading: false, + error: null, }); + //check if a node is a closed goal + function isClosedGoal(node: TreeNodeDesc | null) { + if (!node) return false; + return node.name.toLowerCase().includes("closed goal"); + } + + //Fetches the sequent for a given node using the goal/print API + async function fetchAppliedOn(nodeId:any) { + const options={ + unicode: false, + width: 120, + indentation: 0, + pure: false, + termLabels: true, + }; + + //goalPrint takes a NodeId + const res= await appState.client.goalPrint(nodeId,options); + return res.result as string; + } + + //Opens the context menu when user right-clicks a node function openCtxMenu(e: MouseEvent, node: TreeNodeDesc) { e.preventDefault(); + + // If it's a closed goal: don't fetch anything + if (isClosedGoal(node)) { + ctxMenu = { + open: true, + x: e.clientX, + y: e.clientY, + node, + appliedOn: null, + loading: false, + error: null, + }; + return; + } + + //Normal nodes : fetch "AppliedOn" using goalPrint ctxMenu = { open: true, x: e.clientX, y: e.clientY, node, + appliedOn: null, + loading: true, + error:null, }; + + //Fetch the sequent in the background + fetchAppliedOn(node.id).then(text=> { + if(!ctxMenu.open || ctxMenu.node?.id.nodeId !== node.id.nodeId) return; + + ctxMenu.appliedOn = text; + ctxMenu.loading = false; + }).catch(err => { + if (!ctxMenu.open || ctxMenu.node?.id.nodeId !==node.id.nodeId) return; + + ctxMenu.error = err?.toString?.() ?? "Unknown error"; + ctxMenu.loading = false; + }); + } function closeCtxMenu() { @@ -130,18 +192,42 @@ {/each} {#if ctxMenu.open} -
-
e.stopPropagation()} - > -
Node {ctxMenu.node?.id.nodeId}
- - - -
+
+
e.stopPropagation()} + > + {#if ctxMenu.node?.name?.toLowerCase() === "closed goal"} + +
A closed goal
+ {:else} + +
Taclet info
+ +
+
+
Rule
+
{ctxMenu.node?.name ?? "-"}
+
+ +
+ +
Applied on
+ + {#if ctxMenu.loading} +
Loading…
+ {:else if ctxMenu.error} +
{ctxMenu.error}
+ {:else} +
{ctxMenu.appliedOn ?? "-"}
+ {/if} +
+ {/if}
- {/if} +
+{/if} +
+ \ No newline at end of file diff --git a/src/routes/+page.svelte b/src/routes/+page.svelte index c03edb6..fede7f0 100644 --- a/src/routes/+page.svelte +++ b/src/routes/+page.svelte @@ -10,7 +10,7 @@ import type { ProofId, NodeId } from './api'; import Modal from './Modal.svelte'; - import { ReactiveSignal } from '$lib/reactive.ts'; + import { ReactiveSignal } from '$lib/reactive'; import { writable, type Writable } from "svelte/store"; type AppState = { @@ -28,6 +28,7 @@ proof: null, active_node:null, proofTreeChanged: new ReactiveSignal(), + }); let errorState: string | null = $state(null); @@ -41,7 +42,7 @@ fn main() {
-
(errorState = error)} /> +
(errorState = error)} /> {#if errorState} (errorState = null)}> diff --git a/src/routes/api.ts b/src/routes/api.ts index a017890..d86ad10 100644 --- a/src/routes/api.ts +++ b/src/routes/api.ts @@ -80,8 +80,11 @@ export class Client { return await this.send("proof/auto", [proof, options_framed]); } + + } +//Custom error class for API errors class ApiError { code: number = 0; data: string = ""; @@ -171,3 +174,7 @@ export type ProofStatus = { openGoals: number; closeGoals: number; }; + + + + From f850e6e3b7e2d44345d7bba36d9c33fa3825d99a Mon Sep 17 00:00:00 2001 From: RanimZayen Date: Wed, 28 Jan 2026 23:08:34 +0100 Subject: [PATCH 2/2] Potential fix: adjust parse_message to reload proof tree --- src-tauri/src/prover.rs | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src-tauri/src/prover.rs b/src-tauri/src/prover.rs index 70fd66f..919580d 100644 --- a/src-tauri/src/prover.rs +++ b/src-tauri/src/prover.rs @@ -259,12 +259,19 @@ enum ParseError { } fn parse_message(data: &[u8]) -> Result<(&[u8], usize), ParseError> { + // 1) Find the beginning of a real JSON-RPC message + let start = match memchr::memmem::find(data, b"Content-Length: ") { + Some(i) => i, + None => return Err(ParseError::NeedMoreData), + }; + + // 2) Parse starting from Content-Length, ignoring junk before let mut parser = Parser { - data, - bytes_read: 0, + data: &data[start..], + bytes_read: start, }; - // We cannot parse the header until complete. + // Wait until full header is available if memchr::memmem::find(parser.data, b"\r\n\r\n").is_none() { return Err(ParseError::NeedMoreData); } @@ -282,6 +289,8 @@ fn parse_message(data: &[u8]) -> Result<(&[u8], usize), ParseError> { Ok((payload, parser.bytes_read)) } + + #[derive(Clone, Debug)] struct Parser<'a> { data: &'a [u8],