Potential prover fix for proof tree reload

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],

src/lib/components/ProofTree.svelte

@@ -10,28 +10,90 @@
 
   let nodes = $state<Node[]>([]);
 
+  //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<CtxMenuState>({
     open: false,
     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}
   </ul>
   {#if ctxMenu.open}
-    <div class="ctx-backdrop" onclick={closeCtxMenu}>
-      <div
-        class="ctx-menu"
-        onclick={(e) => e.stopPropagation()}
-      >
-        <div class="ctx-title">Node {ctxMenu.node?.id.nodeId}</div>
-        <button class="ctx-item" disabled>Action A</button>
-        <button class="ctx-item" disabled> Action B</button>
-        <button class="ctx-item" disabled> Action C</button>
-      </div>
+  <div class="ctx-backdrop" onclick={closeCtxMenu}>
+    <div
+      class="ctx-menu"
+      style="left:{ctxMenu.x}px; top:{ctxMenu.y}px;"
+      onclick={(e) => e.stopPropagation()}
+    >
+      {#if ctxMenu.node?.name?.toLowerCase() === "closed goal"}
+
+        <div class="ctx-simple">A closed goal</div>
+      {:else}
+
+        <div class="ctx-title">Taclet info</div>
+
+        <div class="ctx-content">
+          <div class="ctx-row">
+            <div class="ctx-label">Rule</div>
+            <div class="ctx-value">{ctxMenu.node?.name ?? "-"}</div>
+          </div>
+
+          <div class="ctx-sep"></div>
+
+          <div class="ctx-label">Applied on</div>
+
+          {#if ctxMenu.loading}
+            <div class="ctx-mono loading">Loading…</div>
+          {:else if ctxMenu.error}
+            <div class="ctx-mono error">{ctxMenu.error}</div>
+          {:else}
+            <div class="ctx-mono">{ctxMenu.appliedOn ?? "-"}</div>
+          {/if}
+        </div>
+      {/if}
     </div>
-  {/if}
+  </div>
+{/if}
+
 </div>
 
 <style>
@@ -166,10 +252,12 @@
     background: #2b2b2b;
     font-weight: 600;
     cursor: pointer;
+    transition: border-color 120ms ease, transform 120ms ease;
   }
 
   .node:hover {
     border-color: rgba(255, 255, 255, 0.22);
+    transform: translateY(-1px);
   }
 
   .open { background: #662222; }
@@ -181,41 +269,88 @@
     inset: 0;
     z-index: 999;
   }
+  .ctx-simple {
+  padding: 10px 12px;
+  font-size: 13px;
+  font-weight: 600;
+  opacity: 0.95;
+  white-space: nowrap;
+}
 
   .ctx-menu {
     position: fixed;
     z-index: 1000;
-    min-width: 220px;
-    background: #1f1f1f;
-    border: 1px solid #444;
-    border-radius: 8px;
-    padding: 8px;
-    box-shadow: 0 10px 25px rgba(0,0,0,0.4);
+    min-width: 260px;
+    max-width: 420px;
+    background:rgba(20, 20, 20, 0.92);
+    border: 1px solid rgba(255, 255, 255, 0.10);
+    border-radius: 12px;
+    padding: 10px 12px;
+    box-shadow: 0 18px 45px rgba(0,0,0,0.55);
+    backdrop-filter: blur(10px);
+    transform: translate(8px,8px);
   }
 
   .ctx-title {
     font-size: 12px;
-    opacity: 0.8;
-    padding: 6px 8px;
-    border-bottom: 1px solid #333;
-    margin-bottom: 6px;
-  }
-
-  .ctx-item {
-    width: 100%;
-    text-align: left;
-    padding: 8px;
-    border: 0;
-    background: transparent;
-    color: white;
-    cursor: not-allowed;
-    border-radius: 6px;
-    opacity: 0.7;
+    font-weight: 700;
+    letter-spacing: 0.2px;
+    opacity: 0.9;
+    padding: 6px 2px 10px 2px;
+    border-bottom: 1px solid rgba(255,255,255,0.08);
+    margin-bottom: 10px;
   }
 
-  .ctx-item:hover {
-    background: #2b2b2b;
-  }
+  .ctx-content {
+  display: grid;
+  gap: 10px;
+}
+
+.ctx-row {
+  display: grid;
+  grid-template-columns: 92px 1fr;
+  gap: 10px;
+  align-items: baseline;
+}
+
+.ctx-label {
+  font-size: 12px;
+  opacity: 0.7;
+}
+
+.ctx-value {
+  font-size: 13px;
+  font-weight: 650;
+}
+
+.ctx-sep {
+  height: 1px;
+  background: rgba(255,255,255,0.08);
+  margin: 2px 0;
+}
+
+.ctx-mono {
+  font-family: ui-monospace, SFMono-Regular, Menlo, Monaco, Consolas, "Liberation Mono", "Courier New", monospace;
+  font-size: 12px;
+  line-height: 1.35;
+
+  white-space: pre-wrap;
+  word-break: break-word;
+
+  padding: 8px 10px;
+  border-radius: 10px;
+  background: rgba(255,255,255,0.06);
+  border: 1px solid rgba(255,255,255,0.08);
+}
+
+.ctx-mono.loading {
+  opacity: 0.75;
+}
+
+.ctx-mono.error {
+  border-color: rgba(255, 120, 120, 0.35);
+  background: rgba(255, 120, 120, 0.10);
+}
 
   /* Active node = very visible */
   .node.active {
@@ -250,4 +385,4 @@
   .node.closed.active {
     opacity: 0.9;
   }
-</style>
+</style>

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() {
 </script>
 
 <main class="container">
-  <Header {appState} onError={(error) => (errorState = error)} />
+  <Header {appState} onError={(error:any) => (errorState = error)} />
   <!-- <Api /> -->
    {#if errorState}
     <Modal open={true} on:close={() => (errorState = null)}>

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;
 };
+
+
+
+