Skip to content

Commit 80424c2

Browse files
jackeownjackeown
committed
made it work on mobile I think
1 parent 187e7b3 commit 80424c2

3 files changed

Lines changed: 282 additions & 11 deletions

File tree

‎docusaurus-site/src/components/ProofSearchCanvas.js‎

Lines changed: 251 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@ const LIGHT_COLORS = {
1616
tooltipBg: 'rgba(15, 24, 44, 0.9)',
1717
tooltipStroke: 'rgba(255,255,255,0.15)',
1818
tooltipText: '#f5f7ff',
19+
subsumed: '#ff6b6b',
20+
highlight: '#ffe75a',
1921
};
2022

2123
const DARK_COLORS = {
@@ -33,6 +35,8 @@ const DARK_COLORS = {
3335
tooltipBg: 'rgba(20, 27, 44, 0.92)',
3436
tooltipStroke: 'rgba(255,255,255,0.2)',
3537
tooltipText: '#e6edf7',
38+
subsumed: '#ff6b6b',
39+
highlight: '#ffe75a',
3640
};
3741

3842
function getPalette(theme) {
@@ -113,6 +117,9 @@ export default function ProofSearchCanvas({
113117
id,
114118
text: clause.text || '',
115119
status: clause.status || 'new',
120+
prevStatus: null,
121+
statusChangedAt: now,
122+
subsumed: Boolean(clause.subsumed),
116123
x: baseX + Math.cos(angle) * radius,
117124
y: baseY + Math.sin(angle) * radius,
118125
vx: 0,
@@ -122,7 +129,21 @@ export default function ProofSearchCanvas({
122129
} else {
123130
const node = map.get(id);
124131
node.text = clause.text || node.text;
125-
node.status = clause.status || node.status;
132+
const nextStatus = clause.status || node.status;
133+
if (nextStatus !== node.status) {
134+
if (
135+
node.status === 'new' &&
136+
nextStatus === 'passive' &&
137+
typeof window !== 'undefined'
138+
) {
139+
// eslint-disable-next-line no-console
140+
console.log(`[viz] clause ${node.id} new -> passive`);
141+
}
142+
node.prevStatus = node.status;
143+
node.status = nextStatus;
144+
node.statusChangedAt = now;
145+
}
146+
node.subsumed = Boolean(clause.subsumed);
126147
}
127148
});
128149
// Remove nodes that are no longer in the current clause set
@@ -277,6 +298,7 @@ export default function ProofSearchCanvas({
277298
if (!dragging) {
278299
const target = targets.get(String(node.id));
279300
if (target) {
301+
// Pull back to the layout position.
280302
node.vx += (target.x - node.x) * 0.02;
281303
node.vy += (target.y - node.y) * 0.02;
282304
} else {
@@ -296,6 +318,8 @@ export default function ProofSearchCanvas({
296318

297319
// Directed edges from parents to children
298320
const edgeList = edgesRef.current;
321+
const hoverId = hoverRef.current?.node?.id;
322+
const highlight = hoverId ? computeHighlightSets(hoverId, edgeList) : null;
299323
if (edgeList && edgeList.length) {
300324
ctx.strokeStyle = palette.link;
301325
ctx.lineWidth = 1.4;
@@ -308,22 +332,81 @@ export default function ProofSearchCanvas({
308332
if (!from || !to) continue;
309333
drawArrow(ctx, from.x, from.y, to.x, to.y);
310334
}
335+
if (highlight?.edgeKeys?.size) {
336+
ctx.save();
337+
ctx.strokeStyle = palette.highlight;
338+
ctx.lineWidth = 3;
339+
ctx.globalAlpha = 0.5;
340+
ctx.shadowColor = palette.highlight;
341+
ctx.shadowBlur = 16;
342+
ctx.shadowOffsetX = 0;
343+
ctx.shadowOffsetY = 0;
344+
for (let i = 0; i < edgeList.length; i += step) {
345+
const edge = edgeList[i];
346+
if (!highlight.edgeKeys.has(`${edge.from}->${edge.to}`)) continue;
347+
const from = nodeMap.get(String(edge.from));
348+
const to = nodeMap.get(String(edge.to));
349+
if (!from || !to) continue;
350+
drawArrow(ctx, from.x, from.y, to.x, to.y);
351+
}
352+
ctx.strokeStyle = palette.link;
353+
ctx.lineWidth = 1.6;
354+
ctx.globalAlpha = 0.95;
355+
ctx.shadowBlur = 0;
356+
for (let i = 0; i < edgeList.length; i += step) {
357+
const edge = edgeList[i];
358+
if (!highlight.edgeKeys.has(`${edge.from}->${edge.to}`)) continue;
359+
const from = nodeMap.get(String(edge.from));
360+
const to = nodeMap.get(String(edge.to));
361+
if (!from || !to) continue;
362+
drawArrow(ctx, from.x, from.y, to.x, to.y);
363+
}
364+
ctx.restore();
365+
}
311366
}
312367

313368
// Nodes
314-
const hoverId = hoverRef.current?.node?.id;
315369
nodes.forEach((node) => {
316370
const age = (ts - node.bornAt) / 1000;
317-
const pulse = awaitingInput ? 1 + 0.06 * Math.sin(ts / 280 + Number(node.id) * 0.3) : 1;
318-
const baseRadius = 16 + Math.min(18, (node.text?.length || 0) * 0.15);
371+
const pulse = awaitingInput && node.status === 'passive'
372+
? 1 + 0.06 * Math.sin(ts / 280 + Number(node.id) * 0.3)
373+
: 1;
374+
const baseRadius = 18;
319375
const hoverScale = node.id === hoverId ? 1.12 : 1;
320376
const radius = baseRadius * hoverScale;
321-
const color = node.id === String(selectedId)
377+
let color = node.id === String(selectedId)
322378
? palette.selected
323379
: (palette[node.status] || palette.default);
380+
if (node.prevStatus && node.prevStatus !== node.status && node.id !== String(selectedId)) {
381+
const prev = palette[node.prevStatus] || palette.default;
382+
const t = clamp((ts - (node.statusChangedAt || ts)) / 1500, 0, 1);
383+
color = mixColor(prev, color, t);
384+
if (t >= 1) {
385+
node.prevStatus = null;
386+
}
387+
}
388+
389+
if (highlight?.nodes?.has(String(node.id))) {
390+
const inner = radius * pulse + 2;
391+
const outer = radius * pulse + 20;
392+
const grad = ctx.createRadialGradient(node.x, node.y, inner, node.x, node.y, outer);
393+
grad.addColorStop(0, rgbaFrom(palette.highlight, 0.75));
394+
grad.addColorStop(0.5, rgbaFrom(palette.highlight, 0.35));
395+
grad.addColorStop(1, rgbaFrom(palette.highlight, 0));
396+
ctx.globalAlpha = 1;
397+
ctx.fillStyle = grad;
398+
ctx.beginPath();
399+
ctx.arc(node.x, node.y, outer, 0, Math.PI * 2);
400+
ctx.fill();
401+
}
324402

325403
ctx.beginPath();
326-
ctx.fillStyle = color;
404+
const isFalse = isFalseClause(node.text);
405+
if (isFalse) {
406+
ctx.fillStyle = themeRef.current === 'dark' ? '#000000' : '#ffffff';
407+
} else {
408+
ctx.fillStyle = color;
409+
}
327410
ctx.globalAlpha = 0.95;
328411
ctx.arc(node.x, node.y, radius * pulse, 0, Math.PI * 2);
329412
ctx.fill();
@@ -336,6 +419,29 @@ export default function ProofSearchCanvas({
336419
ctx.arc(node.x, node.y, radius * pulse + 6, 0, Math.PI * 2);
337420
ctx.stroke();
338421

422+
if (!node.subsumed) {
423+
ctx.save();
424+
ctx.globalAlpha = 0.7;
425+
ctx.strokeStyle = themeRef.current === 'dark' ? '#ffffff' : '#000000';
426+
ctx.lineWidth = 1.2;
427+
ctx.beginPath();
428+
ctx.arc(node.x, node.y, radius * pulse + 1, 0, Math.PI * 2);
429+
ctx.stroke();
430+
ctx.restore();
431+
}
432+
433+
if (node.subsumed) {
434+
ctx.save();
435+
ctx.globalAlpha = 0.85;
436+
ctx.strokeStyle = palette.subsumed;
437+
ctx.lineWidth = 2.2;
438+
ctx.setLineDash([5, 4]);
439+
ctx.beginPath();
440+
ctx.arc(node.x, node.y, radius * pulse + 2, 0, Math.PI * 2);
441+
ctx.stroke();
442+
ctx.restore();
443+
}
444+
339445
// Label
340446
ctx.globalAlpha = 1;
341447
ctx.fillStyle = palette.text;
@@ -344,7 +450,21 @@ export default function ProofSearchCanvas({
344450
ctx.font = `600 ${fontPx}px system-ui, sans-serif`;
345451
ctx.textAlign = 'center';
346452
ctx.textBaseline = 'middle';
347-
ctx.fillText(node.id, node.x, node.y);
453+
if (isFalse) {
454+
const trophySize = Math.max(12, 10 / zoom);
455+
const gap = Math.max(4, 3 / zoom);
456+
const total = trophySize + gap + fontPx;
457+
const startY = node.y - total / 2;
458+
const trophyY = startY + trophySize / 2;
459+
const idY = startY + trophySize + gap + fontPx / 2;
460+
ctx.textBaseline = 'middle';
461+
ctx.fillText(node.id, node.x, idY);
462+
ctx.font = `${trophySize}px "Apple Color Emoji","Segoe UI Emoji","Noto Color Emoji",sans-serif`;
463+
ctx.textBaseline = 'middle';
464+
ctx.fillText('🏆', node.x, trophyY);
465+
} else {
466+
ctx.fillText(node.id, node.x, node.y);
467+
}
348468
});
349469

350470
// Hover tooltip
@@ -492,6 +612,12 @@ export default function ProofSearchCanvas({
492612
};
493613
const handleUp = (ev) => {
494614
if (ev?.pointerType === 'touch') return;
615+
const state = dragRef.current;
616+
if (state && state.type === 'node' && state.dragging) {
617+
const node = nodesRef.current.get(state.id);
618+
if (node) {
619+
}
620+
}
495621
dragRef.current = null;
496622
canvas.style.cursor = 'grab';
497623
};
@@ -665,6 +791,11 @@ export default function ProofSearchCanvas({
665791
}
666792
}
667793
}
794+
if (state && state.type === 'node' && state.dragging) {
795+
const node = nodesRef.current.get(state.id);
796+
if (node) {
797+
}
798+
}
668799
dragRef.current = null;
669800
canvas.style.cursor = 'grab';
670801
};
@@ -762,6 +893,57 @@ function drawArrow(ctx, x1, y1, x2, y2) {
762893
ctx.fill();
763894
}
764895

896+
function computeHighlightSets(rootId, edges) {
897+
const parents = new Map();
898+
const children = new Map();
899+
edges.forEach((edge) => {
900+
const from = String(edge.from);
901+
const to = String(edge.to);
902+
if (!parents.has(to)) parents.set(to, new Set());
903+
parents.get(to).add(from);
904+
if (!children.has(from)) children.set(from, new Set());
905+
children.get(from).add(to);
906+
});
907+
908+
const root = String(rootId);
909+
const ancestors = new Set();
910+
const descendants = new Set();
911+
const edgeKeys = new Set();
912+
913+
// Walk up: collect only edges on paths to ancestors
914+
const queueUp = [root];
915+
while (queueUp.length) {
916+
const current = queueUp.pop();
917+
const ps = parents.get(current);
918+
if (!ps) continue;
919+
ps.forEach((p) => {
920+
edgeKeys.add(`${p}->${current}`);
921+
if (!ancestors.has(p)) {
922+
ancestors.add(p);
923+
queueUp.push(p);
924+
}
925+
});
926+
}
927+
928+
// Walk down: collect only edges on paths to descendants
929+
const queueDown = [root];
930+
while (queueDown.length) {
931+
const current = queueDown.pop();
932+
const cs = children.get(current);
933+
if (!cs) continue;
934+
cs.forEach((c) => {
935+
edgeKeys.add(`${current}->${c}`);
936+
if (!descendants.has(c)) {
937+
descendants.add(c);
938+
queueDown.push(c);
939+
}
940+
});
941+
}
942+
943+
const nodes = new Set([root, ...ancestors, ...descendants]);
944+
return {nodes, ancestors, descendants, edgeKeys};
945+
}
946+
765947
function computeTargets(nodes, edges, width, height, layoutMode, minX = 0, minY = 0) {
766948
const centerX = minX + width * 0.5;
767949
const centerY = minY + height * 0.5;
@@ -846,18 +1028,22 @@ function computeTargets(nodes, edges, width, height, layoutMode, minX = 0, minY
8461028
const usableH = Math.max(1, height - topPad - bottomPad);
8471029
const cols = statusOrder.length;
8481030
const stepX = cols > 1 ? usableW / (cols - 1) : 0;
1031+
const columnTargets = new Map();
8491032
groups.forEach((layer, d) => {
8501033
if (!layer.length) return;
8511034
layer.sort((a, b) => String(a.id).localeCompare(String(b.id)));
8521035
layer.forEach((node, idx) => {
8531036
const t = (idx + 1) / (layer.length + 1);
8541037
const jitter = (seededRandom(`${node.id}:jy`) - 0.5) * 0.08;
855-
targets.set(String(node.id), {
1038+
const target = {
8561039
x: minX + leftPad + stepX * d,
8571040
y: minY + topPad + usableH * clamp(t + jitter, 0.05, 0.95),
858-
});
1041+
};
1042+
targets.set(String(node.id), target);
1043+
columnTargets.set(String(node.id), {x: target.x, y: target.y});
8591044
});
8601045
});
1046+
targets._columnTargets = columnTargets;
8611047
return targets;
8621048
}
8631049

@@ -876,18 +1062,22 @@ function computeTargets(nodes, edges, width, height, layoutMode, minX = 0, minY
8761062
const usableW = Math.max(1, width - leftPad - rightPad);
8771063
const usableH = Math.max(1, height - topPad - bottomPad);
8781064
const stepX = maxDepth > 0 ? usableW / maxDepth : 0;
1065+
const columnTargets = new Map();
8791066
layers.forEach((layer, d) => {
8801067
if (!layer.length) return;
8811068
layer.sort((a, b) => String(a.id).localeCompare(String(b.id)));
8821069
layer.forEach((node, idx) => {
8831070
const t = (idx + 1) / (layer.length + 1);
8841071
const jitter = (seededRandom(`${node.id}:jy`) - 0.5) * 0.08;
885-
targets.set(String(node.id), {
1072+
const target = {
8861073
x: minX + leftPad + stepX * d,
8871074
y: minY + topPad + usableH * clamp(t + jitter, 0.05, 0.95),
888-
});
1075+
};
1076+
targets.set(String(node.id), target);
1077+
columnTargets.set(String(node.id), {x: target.x, y: target.y});
8891078
});
8901079
});
1080+
targets._columnTargets = columnTargets;
8911081
return targets;
8921082
}
8931083

@@ -927,6 +1117,56 @@ function drawRoundedRect(ctx, x, y, w, h, r) {
9271117
ctx.closePath();
9281118
}
9291119

1120+
function isFalseClause(text) {
1121+
return /\$false\b/i.test(String(text || '').trim());
1122+
}
1123+
1124+
function mixColor(a, b, t) {
1125+
const c1 = toRgb(a);
1126+
const c2 = toRgb(b);
1127+
const r = Math.round(lerp(c1.r, c2.r, t));
1128+
const g = Math.round(lerp(c1.g, c2.g, t));
1129+
const bch = Math.round(lerp(c1.b, c2.b, t));
1130+
return `rgb(${r}, ${g}, ${bch})`;
1131+
}
1132+
1133+
function rgbaFrom(color, alpha) {
1134+
const c = toRgb(color);
1135+
return `rgba(${c.r}, ${c.g}, ${c.b}, ${alpha})`;
1136+
}
1137+
1138+
function toRgb(color) {
1139+
if (!color) return {r: 0, g: 0, b: 0};
1140+
if (color.startsWith('#')) {
1141+
const hex = color.slice(1);
1142+
if (hex.length === 3) {
1143+
return {
1144+
r: parseInt(hex[0] + hex[0], 16),
1145+
g: parseInt(hex[1] + hex[1], 16),
1146+
b: parseInt(hex[2] + hex[2], 16),
1147+
};
1148+
}
1149+
if (hex.length === 6) {
1150+
return {
1151+
r: parseInt(hex.slice(0, 2), 16),
1152+
g: parseInt(hex.slice(2, 4), 16),
1153+
b: parseInt(hex.slice(4, 6), 16),
1154+
};
1155+
}
1156+
} else if (color.startsWith('rgb')) {
1157+
const match = color.match(/rgba?\(([^)]+)\)/i);
1158+
if (match) {
1159+
const parts = match[1].split(',').map((p) => parseFloat(p.trim()));
1160+
return {
1161+
r: Math.max(0, Math.min(255, parts[0] || 0)),
1162+
g: Math.max(0, Math.min(255, parts[1] || 0)),
1163+
b: Math.max(0, Math.min(255, parts[2] || 0)),
1164+
};
1165+
}
1166+
}
1167+
return {r: 0, g: 0, b: 0};
1168+
}
1169+
9301170
function seededRandom(seed) {
9311171
let h = 2166136261;
9321172
const str = String(seed);

0 commit comments

Comments
 (0)