diff --git a/web/src/components/Navbar.tsx b/web/src/components/Navbar.tsx index 600b7858..31a6e02b 100644 --- a/web/src/components/Navbar.tsx +++ b/web/src/components/Navbar.tsx @@ -22,9 +22,25 @@ export function Navbar() { href="https://github.com/MathNetwork/OpenGA" target="_blank" rel="noopener noreferrer" + aria-label="GitHub" + title="GitHub" className="hover:text-white/75 transition-colors" > - GitHub + + + + diff --git a/web/src/panels/workspace/NetworkView.tsx b/web/src/panels/workspace/NetworkView.tsx index d91bf291..6424c687 100644 --- a/web/src/panels/workspace/NetworkView.tsx +++ b/web/src/panels/workspace/NetworkView.tsx @@ -26,6 +26,13 @@ import { getSortFill, parseSortFromRecord } from '@/lib/sortColors' import { NetworkSettings } from './NetworkSettings' import { usePluginStore } from '@/plugins/registry' +// 常规节点半径(refView 的 degreeRadius 基准值)——连线粗细以此为锚等比缩放。 +const BASE_NODE_RADIUS = 8 +// 连线粗细 = 常规节点半径的固定比例(世界单位),随缩放与节点同步放大。 +const LINK_WIDTH_RATIO = 0.1 +// 默认连线颜色:亮灰色。 +const LINK_COLOR = 'rgba(200,200,210,0.5)' + // ── ref 模式箭头绘制 ── function drawArrow(ctx: CanvasRenderingContext2D, sx: number, sy: number, tx: number, ty: number, headLen: number) { const dx = tx - sx @@ -109,7 +116,7 @@ export const NetworkView = memo(function NetworkView() { const hoveredNode = hoveredNodeRef.current - // ── Draw links (directed arrows) ── + // ── Draw links (thin lines; arrow only on selected edges) ── for (const link of linksRef.current) { const s = link.source as ForceNode const t = link.target as ForceNode @@ -133,16 +140,20 @@ export const NetworkView = memo(function NetworkView() { ctx.beginPath() ctx.moveTo(ax, ay) ctx.lineTo(bx, by) - const edgeColor = link.color || 'rgba(255,255,255,0.15)' + const edgeColor = link.color || LINK_COLOR ctx.strokeStyle = isSelected ? 'rgba(255,255,255,0.5)' : edgeColor - ctx.lineWidth = (isSelected ? 1.5 : 0.8) / transform.k + // 线宽 = 常规节点半径 × 固定比例(世界单位),随缩放与节点同步。 + ctx.lineWidth = BASE_NODE_RADIUS * LINK_WIDTH_RATIO * (isSelected ? 1.8 : 1) if (link.dashed) ctx.setLineDash([4 / transform.k, 3 / transform.k]) ctx.stroke() if (link.dashed) ctx.setLineDash([]) - const headLen = Math.min(6 / transform.k, len * 0.3) - ctx.fillStyle = isSelected ? 'rgba(255,255,255,0.5)' : edgeColor - drawArrow(ctx, ax, ay, bx, by, headLen) + // 默认就是一条细线;方向箭头仅在选中节点的边上出现。 + if (isSelected) { + const headLen = Math.min(6 / transform.k, len * 0.3) + ctx.fillStyle = 'rgba(255,255,255,0.5)' + drawArrow(ctx, ax, ay, bx, by, headLen) + } ctx.globalAlpha = 1 } @@ -435,7 +446,9 @@ export const NetworkView = memo(function NetworkView() { })) forceLinks = (data.edges || []).map((e: any) => ({ id: e.hash || `${e.source}-${e.target}`, - source: e.source, target: e.target, color: e.color || 'rgba(255,255,255,0.15)', + // sort(默认语义着色)下边统一灰,降噪;选了算法着色 + // (community/depth/pagerank…)时保留后端算出的边色。 + source: e.source, target: e.target, color: colorBy === 'sort' ? LINK_COLOR : (e.color || LINK_COLOR), ...(e.dashed ? { dashed: true } : {}), })) // Propagate colors to ALL atoms (not just filtered) @@ -459,7 +472,7 @@ export const NetworkView = memo(function NetworkView() { })) forceLinks = refLinks.map(l => ({ id: `ref-${l.source}-${l.target}-${l.position}`, - source: l.source, target: l.target, color: 'rgba(255,255,255,0.15)', + source: l.source, target: l.target, color: LINK_COLOR, })) } @@ -588,7 +601,8 @@ export const NetworkView = memo(function NetworkView() { const s = typeof link.source === 'string' ? link.source : (link.source as any).id const t = typeof link.target === 'string' ? link.target : (link.target as any).id const updated = edgeMap[`${s}-${t}`] - if (updated) link.color = updated.color + // 与加载路径一致:sort 模式边统一灰,算法着色时用后端边色。 + if (updated) link.color = colorBy === 'sort' ? LINK_COLOR : (updated.color || LINK_COLOR) } // Just re-render, no simulation restart diff --git a/web/src/plugins/leannets/EntryBlockRenderer.tsx b/web/src/plugins/leannets/EntryBlockRenderer.tsx index da3fb97e..bcdab5d3 100644 --- a/web/src/plugins/leannets/EntryBlockRenderer.tsx +++ b/web/src/plugins/leannets/EntryBlockRenderer.tsx @@ -9,72 +9,97 @@ import { LeanCode } from './LeanHighlight' import { LeanBadge } from './LeanBadge' import { SORT_LABELS, parseRecord } from './utils' -/** Find the cross-source lean counterpart for a tex atom. */ +interface LeanRecord { hash: string; record: Record } +interface LeanIndex { + /** tex atom hash → its cross-source lean counterpart */ + counterpart: Map + /** lean theorem hash → its proof entries */ + proofs: Map +} + +// Per-project lean index, built ONCE from a single atoms+edges fetch and shared +// by every card. Previously each card re-fetched the whole degree-1 edge set +// (megabytes) on mount, twice — the dominant source of read-view lag. Keyed by +// project path; the promise is cached so concurrent mounts dedupe to one build. +const leanIndexCache = new Map>() + +async function buildLeanIndex(projectPath: string): Promise { + const counterpart = new Map() + const proofs = new Map() + const p = encodeURIComponent(projectPath) + try { + const [atomsRes, edgesRes] = await Promise.all([ + fetch(`${API_BASE}/api/astrolabe/entries?path=${p}°ree=0`), + fetch(`${API_BASE}/api/astrolabe/entries?path=${p}°ree=1`), + ]) + const atoms: Record = atomsRes.ok ? await atomsRes.json() : {} + const edges: Record = edgesRes.ok ? await edgesRes.json() : {} + + // Parse atom records once; index source + record for in-memory lookups. + const atomRec = new Map>() + for (const [h, e] of Object.entries(atoms)) { + const rec = parseRecord((e as any).record) + if (rec) atomRec.set(h, rec) + } + const isLean = (h: string) => atomRec.get(h)?.source === 'lean' + + for (const edge of Object.values(edges) as any[]) { + const ref = edge.ref as string[] + if (!ref || ref.length !== 2) continue + const [a, b] = ref + // Cross-source counterpart: exactly one side is lean → map tex→lean. + const aLean = isLean(a), bLean = isLean(b) + if (aLean !== bLean) { + const leanH = aLean ? a : b + const texH = aLean ? b : a + const leanR = atomRec.get(leanH) + if (leanR && !counterpart.has(texH)) counterpart.set(texH, { hash: leanH, record: leanR }) + } + // Proof edge: ref[0] is the lean theorem, sort ends in ", proof)". + if (isLean(ref[0])) { + let sort = '' + try { sort = JSON.parse(edge.record).sort || '' } catch { /* skip */ } + const proofR = sort.endsWith(', proof)') ? atomRec.get(ref[1]) : undefined + if (proofR) { + const list = proofs.get(ref[0]) ?? [] + list.push({ hash: ref[1], record: proofR }) + proofs.set(ref[0], list) + } + } + } + } catch { /* leave index empty on failure */ } + return { counterpart, proofs } +} + +function loadLeanIndex(projectPath: string): Promise { + let cached = leanIndexCache.get(projectPath) + if (!cached) { cached = buildLeanIndex(projectPath); leanIndexCache.set(projectPath, cached) } + return cached +} + +/** Find the cross-source lean counterpart for a tex atom (in-memory lookup). */ function useLeanCounterpart(hash: string, source: string | undefined, projectPath: string) { - const [leanEntry, setLeanEntry] = useState<{ hash: string; record: Record } | null>(null) + const [leanEntry, setLeanEntry] = useState(null) useEffect(() => { if (source !== 'tex' || !hash || !projectPath) { setLeanEntry(null); return } - fetch(`${API_BASE}/api/astrolabe/entries?path=${encodeURIComponent(projectPath)}°ree=1`) - .then(r => r.ok ? r.json() : {}) - .then(async (edges: Record) => { - // Find degree-1 entry where one ref is this hash, other is a lean atom - for (const [, edge] of Object.entries(edges)) { - const ref = (edge as any).ref as string[] - if (ref.length !== 2) continue - const otherHash = ref[0] === hash ? ref[1] : ref[1] === hash ? ref[0] : null - if (!otherHash) continue - try { - const r = await fetch(`${API_BASE}/api/astrolabe/entries/${otherHash}?path=${encodeURIComponent(projectPath)}`) - if (!r.ok) continue - const otherEntry = await r.json() - if (!otherEntry?.record) continue - const parsed = parseRecord(otherEntry.record) - if (parsed?.source === 'lean') { - setLeanEntry({ hash: otherHash, record: parsed }) - return - } - } catch { continue } - } - setLeanEntry(null) - }) - .catch(() => setLeanEntry(null)) + let alive = true + loadLeanIndex(projectPath).then(idx => { if (alive) setLeanEntry(idx.counterpart.get(hash) ?? null) }) + return () => { alive = false } }, [hash, source, projectPath]) return leanEntry } -/** Find proof entries for a lean theorem via (theorem, proof) edges. */ +/** Find proof entries for a lean theorem via (theorem, proof) edges (in-memory). */ function useLeanProofs(leanHash: string | undefined, projectPath: string) { - const [proofEntries, setProofEntries] = useState<{ hash: string; record: Record }[]>([]) + const [proofEntries, setProofEntries] = useState([]) useEffect(() => { if (!leanHash || !projectPath) { setProofEntries([]); return } - fetch(`${API_BASE}/api/astrolabe/entries?path=${encodeURIComponent(projectPath)}°ree=1`) - .then(r => r.ok ? r.json() : {}) - .then(async (edges: Record) => { - const proofHashes: string[] = [] - for (const [, edge] of Object.entries(edges) as [string, any][]) { - if (edge.ref[0] === leanHash) { - try { - const s = JSON.parse(edge.record).sort || '' - if (s.endsWith(', proof)')) proofHashes.push(edge.ref[1]) - } catch { /* skip */ } - } - } - if (proofHashes.length === 0) { setProofEntries([]); return } - const results = await Promise.all(proofHashes.map(async h => { - try { - const r = await fetch(`${API_BASE}/api/astrolabe/entries/${h}?path=${encodeURIComponent(projectPath)}`) - if (!r.ok) return null - const e = await r.json() - if (!e?.record) return null - return { hash: h, record: parseRecord(e.record) } - } catch { return null } - })) - setProofEntries(results.filter((r): r is { hash: string; record: Record } => r !== null)) - }) - .catch(() => setProofEntries([])) + let alive = true + loadLeanIndex(projectPath).then(idx => { if (alive) setProofEntries(idx.proofs.get(leanHash) ?? []) }) + return () => { alive = false } }, [leanHash, projectPath]) return proofEntries