Public
Edited
May 29
url2 = "https://www.github.com/neobourbaki/Library/tree/main/database/"
GITHUB_REPO_API_URL = 'https://api.github.com/repos/neobourbaki/Library/contents/database'
thm_ids = available_ids_data.filter(item => item.name[0] && item.name[0].match(/[A-Z]/)).map(item => item.name)
function nodeType(id) {
if (/^[0-9][0-9A-Z]{7}$/.test(id)) return 'def';
if (/^[A-Z][0-9A-Z]{7}$/.test(id)) return 'thm';
return null;
}
async function getNode(id, tree = {}, generation = 15, label = '', args = {}) {
if (generation <= 0) {
return tree;
}
let initialLabel = label;
if (!tree[id]) {
tree[id] = {
type: /^[0-9]/.test(id) ? 'def' : 'thm',
label: initialLabel,
children: [],
parents: [],
inProcess: false,
failed: false,
fetched: false,
};
} else {
if (initialLabel && tree[id].label === "") {
tree[id].label = initialLabel;
}
}
if (!nodeType(id) && !tree[id].fetched) {
tree[id].failed = true;
return tree;
}
if (tree[id].inProcess || tree[id].fetched) {
return tree;
}
tree[id].inProcess = true;
try {
const response = await fetch(url + `${id}/${id}.json`);
if (response.ok) {
const data = await response.json();
tree[id].data = data;
if (tree[id].label === "" || tree[id].label === id) {
tree[id].label = data.name || id;
}
tree[id].type = data.type_ === 'definition' ? 'def' : (data.type_ === 'theorem' ? 'thm' : tree[id].type);
tree[id].failed = false;
tree[id].fetched = true;
let dependencies = data.dependencies || {};
if (data.type && typeof data.type === 'object' && !Array.isArray(data.type)) {
dependencies = { ...dependencies, ...data.type };
}
const sections = ['statements', 'proofs', 'definitions'];
sections.forEach(section => {
Object.values(data[section] || {}).forEach(item => {
if (item && item.dependencies) {
dependencies = { ...dependencies, ...item.dependencies };
}
});
});
const dependencyPromises = [];
for (let depKey in dependencies) {
let depId = depKey;
let depLabel = dependencies[depKey] || '';
if (!nodeType(depKey) && depLabel && depLabel.includes(':') && depLabel.length > depKey.length) {
const parts = depLabel.split(':');
if (nodeType(parts[0])) {
depId = parts[0];
depLabel = parts.slice(1).join(':').trim();
}
} else if (!nodeType(depKey) && depKey.includes(':')) {
const parts = depKey.split(':');
if (nodeType(parts[0])) {
depId = parts[0];
depLabel = parts.slice(1).join(':').trim() || depLabel;
}
}
if (!tree[id].parents.includes(depId)) {
tree[id].parents.push(depId);
}
if (!tree[depId]) {
tree[depId] = {
type: /^[0-9]/.test(depId) ? 'def' : 'thm',
label: depLabel || depId,
children: [],
parents: [],
inProcess: false,
failed: !nodeType(depId),
fetched: false
};
if (nodeType(depId)) {
dependencyPromises.push(getNode(depId, tree, generation - 1, depLabel || depId));
}
} else {
if (depLabel && (tree[depId].label === depId || tree[depId].label === "")) {
tree[depId].label = depLabel;
}
}
if (!tree[depId].children.includes(id)) {
tree[depId].children.push(id);
}
}
await Promise.all(dependencyPromises);
} else {
tree[id].failed = true;
if (tree[id].label === "") tree[id].label = id + " (failed)";
}
} catch (error) {
tree[id].failed = true;
if (tree[id].label === "") tree[id].label = id + " (error)";
} finally {
tree[id].inProcess = false;
}
return tree;
}
function replaceVariables(obj1, obj2, str1, str2) {
// Function to extract keys from the string pattern {key}
const extractKeys = (text) => {
const regex = /\{(\w+)\}/g;
let keys = [], match;
while ((match = regex.exec(text)) !== null) {
keys.push(match[1]);
}
return keys;
};
// Recursive function to resolve nested keys
const resolveNestedKeys = (value, obj) => {
let resolvedValue = value;
const nestedKeys = extractKeys(resolvedValue);
nestedKeys.forEach(nestedKey => {
if (obj[nestedKey]) {
resolvedValue = resolvedValue.replace(`{${nestedKey}}`, resolveNestedKeys(obj[nestedKey], obj));
}
});
return resolvedValue;
};
// Resolve the values for each key in obj1 first to handle deep nesting
for (let key in obj1) {
obj1[key] = resolveNestedKeys(obj1[key], obj1);
}
// Replace references in obj2 based on keys extracted from str1 and mapped in obj1
const keysInStr1 = extractKeys(str1);
const keysInStr2 = extractKeys(str2);
keysInStr2.forEach((key, index) => {
const obj1Key = keysInStr1[index]; // Corresponding key in obj1
if (obj1[obj1Key]) {
obj2[key] = resolveNestedKeys(obj1[obj1Key], obj1);
}
});
return obj2;
}
// processedTreeToCytoscapeElements function (as provided before)
function processedTreeToCytoscapeElements(processedTree) {
const elements = [];
if (!processedTree || typeof processedTree !== 'object' || Object.keys(processedTree).length === 0) {
// console.warn("processedTreeToCytoscapeElements received empty or invalid tree input.");
return elements; // Return empty array if input is bad
}
const nodeIds = new Set(Object.keys(processedTree));
for (const [id, nodeData] of Object.entries(processedTree)) {
if (!nodeData) { // Skip if nodeData is somehow null/undefined
// console.warn(`Skipping null/undefined nodeData for id: ${id}`);
continue;
}
elements.push({
group: 'nodes',
data: {
id: id,
label: (nodeData.label || id).replace(/--/g, '\n'),
type: nodeData.type || (/^[0-9]/.test(id) ? 'def' : 'thm'),
failed: nodeData.failed || false,
// Add any other data you might want for styling or tooltips
// originalData: nodeData.data // e.g. to store the full fetched JSON
}
});
}
for (const [nodeId, nodeData] of Object.entries(processedTree)) {
if (!nodeData) continue; // Skip if nodeData is somehow null/undefined
if (nodeData.parents && Array.isArray(nodeData.parents)) {
nodeData.parents.forEach(parentId => {
if (nodeIds.has(String(parentId)) && nodeIds.has(String(nodeId))) { // Ensure IDs are strings for lookup if necessary
elements.push({
group: 'edges',
data: {
id: `${parentId}->${nodeId}`,
source: String(parentId), // Ensure source/target are strings if IDs are numbers
target: String(nodeId)
}
});
} else {
// console.warn(`Skipping edge: parent ${parentId} or node ${nodeId} not found in processedTree keys. Existing keys: ${Array.from(nodeIds)}`);
}
});
}
}
return elements;
}
// Cell: graphviz_display (or similar name)
// This cell depends on 'raw_graph_data', 'digraph_function', and 'focus_id'
{
if (!raw_graph_data || Object.keys(raw_graph_data).length === 0) {
if (focus_id) {
return html`<div style="padding: 20px; font-style: italic;">No data loaded for ${focus_id}.</div>`;
} else {
return html`<div style="padding: 20px; font-style: italic;">Select a theorem to display its graph.</div>`;
}
}
// Generate the DOT string using the current data and focus_id
// For this example, no complex highlighting/dimming logic, just focus
const dotString = digraph(raw_graph_data, { focusNodeId: focus_id });
// const dotString = digraph_function(raw_graph_data); // Simplest version
// Render using Observable's dot tag - THIS SHOULD BE ZOOMABLE/PANNABLE BY DEFAULT
// The @hpcc-js/wasm renderer handles this.
const svgOutput = dot`${dotString}`;
// ---- For Click-to-Side-Panel Interaction (Optional, keep it separate first) ----
// If you want to add the side panel later, the JavaScript for that
// would go here, operating on 'svgOutput'.
// For now, let's focus purely on the Graphviz rendering and its default interactivity.
//
// Example of getting the SVG element if needed for JS interaction later:
// Promises.delay(100).then(() => { // Ensure SVG is rendered
// const actualSVGElement = svgOutput.querySelector('svg');
// if (actualSVGElement) {
// console.log("Actual SVG element found:", actualSVGElement);
// // Here you could attach event listeners for the side panel if needed.
// } else {
// // The svgOutput itself might be the <svg> if the renderer is simple.
// // Or it might be a wrapper. Inspect svgOutput in the console.
// console.log("svgOutput from dot tag:", svgOutput);
// }
// });
// ---- End Optional Interaction Block ----
return svgOutput;
}
// Cytoscape Rendering Cell
{
// This cell depends on 'raw_graph_data' and 'cytoscape' (the library)
// It will re-run if raw_graph_data changes (i.e., when focus_id changes and getNode completes)
const currentFocusId = focus_id; // Capture for consistent use within this render
// Display a loading/status message
// The container div will be created first.
const container = html`<div style="width: 100%; height: 700px; border: 1px solid #ccc;"></div>`;
if (!raw_graph_data || Object.keys(raw_graph_data).length === 0) {
if (currentFocusId) { // Only show "no data" if a focus_id was actually selected
container.innerHTML = `<div style="padding: 20px; font-style: italic;">No data loaded for ${currentFocusId}. It might be fetching or an error occurred.</div>`;
} else {
container.innerHTML = `<div style="padding: 20px; font-style: italic;">Select a theorem to display its dependency graph.</div>`;
}
return container; // Return the container with the message
}
// console.log("[Render Cell] Received raw_graph_data:", JSON.parse(JSON.stringify(raw_graph_data)));
let cytoscapeElements;
try {
cytoscapeElements = processedTreeToCytoscapeElements(raw_graph_data);
// console.log("[Render Cell] Transformed cytoscapeElements (first 5):", JSON.stringify(cytoscapeElements.slice(0,5), null, 2));
// console.log(`[Render Cell] Total elements: ${cytoscapeElements.length}, Nodes: ${cytoscapeElements.filter(e=>e.group==='nodes').length}, Edges: ${cytoscapeElements.filter(e=>e.group==='edges').length}`);
// Basic validation of transformed elements
if (!Array.isArray(cytoscapeElements)) throw new Error("Transformation did not produce an array.");
for (const el of cytoscapeElements) {
if (!el || !el.group || !el.data || !el.data.id) throw new Error(`Malformed element: ${JSON.stringify(el)}`);
if (el.group === 'edges' && (!el.data.source || !el.data.target)) throw new Error(`Malformed edge: ${JSON.stringify(el)}`);
}
} catch (e) {
console.error("[Render Cell] Error during data transformation or validation:", e);
container.innerHTML = `<div style="color:red; padding:20px;">Error preparing graph data: ${e.message}. Check console.</div>`;
return container;
}
if (cytoscapeElements.filter(el => el.group === 'nodes').length === 0 && Object.keys(raw_graph_data).length > 0) {
container.innerHTML = `<div style="padding: 20px; font-style: italic;">Data loaded for ${currentFocusId}, but no visualizable nodes were generated. Check transformation logic.</div>`;
return container;
}
if (cytoscapeElements.length === 0 && Object.keys(raw_graph_data).length === 0 && currentFocusId) {
// This case is handled by the earlier check on raw_graph_data
}
// Initialize Cytoscape
try {
// console.log("[Render Cell] Initializing Cytoscape instance.");
const cyInstance = cytoscape({
container: container, // The div created above
elements: cytoscapeElements,
style: [
{
selector: 'node',
style: {
'background-color': (ele) => ele.data('failed') ? 'orangered' : (ele.data('type') === 'def' ? '#5bc0de' : '#62c370'),
'label': 'data(label)',
'text-valign': 'center', 'text-halign': 'center',
'font-size': '10px', 'color': 'black',
'text-wrap': 'wrap', 'text-max-width': '80px',
'width': 'label', 'height': 'label', 'padding': '8px',
'shape': (ele) => ele.data('type') === 'def' ? 'round-rectangle' : 'ellipse',
'border-width': (ele) => ele.data('id') === currentFocusId ? 2.5 : 0.8,
'border-color': (ele) => ele.data('id') === currentFocusId ? 'blue' : (ele.data('failed') ? 'darkred' : '#555'),
'opacity': (ele) => (ele.data('id') === currentFocusId || !ele.data('failed')) ? 1 : 0.7, // Fade failed nodes slightly
}
},
{
selector: 'edge',
style: {
'width': 1.2,
'line-color': '#999',
'target-arrow-color': '#999',
'target-arrow-shape': 'triangle',
'arrow-scale': 0.7,
'curve-style': 'bezier', // Or 'straight', 'segments', 'taxi', 'haystack'
// 'haystack-radius': 0, // for haystack edges
}
}
],
layout: {
name: 'cose', // Default to cose
// name: 'breadthfirst', // Alternative: good for hierarchies
// rankDir: 'TB', // For breadthfirst or dagre: 'TB' or 'LR'
// roots: `[id = "${currentFocusId}"]`, // For breadthfirst: start from the focus_id
fit: true,
padding: 30,
// Cose specific:
idealEdgeLength: 90, nodeOverlap: 15, refresh: 20, randomize: false,
componentSpacing: 80, nodeRepulsion: (node) => 300000, edgeElasticity: (edge) => 90,
// Breadthfirst specific:
// directed: true, circle: false, grid: false, spacingFactor: 1.2,
},
zoom: 1, minZoom: 0.05, maxZoom: 5,
zoomingEnabled: true, userZoomingEnabled: true,
panningEnabled: true, userPanningEnabled: true,
boxSelectionEnabled: false,
});
// Optional: Add event listeners or further interactions
// cyInstance.on('tap', 'node', function(evt){
// var node = evt.target;
// console.log( 'tapped ' + node.id(), node.data() );
// // You could potentially set focus_id here to navigate
// // mutable focus_id = node.id(); // If you define focus_id as mutable
// });
} catch (e) {
console.error("[Render Cell] Error initializing Cytoscape instance:", e);
container.innerHTML = `<div style="color:red; padding:20px;">Cytoscape Error: ${e.message}. Check console.</div>`;
}
return container; // Return the container, now populated by Cytoscape
}
// Cell: digraph_function
function digraph(tree, { focusNodeId = null, highlightedNodes = [], dimmedNodes = [] } = {}) {
// Helper function to find all paths from source to target (if needed for reduction)
// function findAllPaths(...) { ... }
// Function to reduce graph by removing implied links (if using)
// function reducedGraph(tree) { ... }
let dotstring = 'digraph dependencies {\n';
dotstring += ' graph [splines=true overlap=false concentrate=true];\n'; // concentrate=true can help with edge clutter
dotstring += ' rankdir=TB;\n';
dotstring += ' node [fontname="sans-serif" fontsize=10];\n'; // Base fontsize
dotstring += ' edge [fontname="sans-serif" fontsize=9];\n';
// Define nodes
Object.entries(tree).forEach(([id, node]) => {
if (!node) {
console.warn(`Node data for ID '${id}' is missing in the tree.`);
return; // Skip this problematic node
}
let shape = node.type === 'def' ? 'box' : 'ellipse';
let label = typeof node.label === 'string' ? node.label.replace(/"/g, '\\"').replace(/--/g, '\\n ') : id;
let color = node.failed ? 'red' : 'black';
let fillcolor = "white"; // Default fill
let style = "filled"; // To make fillcolor effective
let penwidth = 1;
let fontcolor = "black";
// Example: Highlighting logic (can be expanded)
if (id === focusNodeId) {
color = "blue";
fillcolor = "#e6f0ff"; // Light blue
penwidth = 2.5;
} else if (highlightedNodes.includes(id)) {
color = "darkgreen";
fillcolor = "#e6ffe6"; // Light green
penwidth = 1.5;
} else if (dimmedNodes.length > 0 && !dimmedNodes.includes(id) && id !== focusNodeId && !highlightedNodes.includes(id)) {
// If dimming is active and this node is not focus/highlighted, dim it
color = "lightgray";
fontcolor = "gray";
fillcolor = "#f5f5f5";
}
dotstring += ` "${id}" [label="${label}", tooltip="${id}:\\n${label.replace(/\\n/g, ' ')}", shape=${shape}, color="${color}", fillcolor="${fillcolor}", style="${style}", fontcolor="${fontcolor}", penwidth=${penwidth}];\n`;
});
// Define edges (using direct parents from your tree structure)
Object.entries(tree).forEach(([nodeId, nodeData]) => {
if (nodeData && nodeData.parents && Array.isArray(nodeData.parents)) {
nodeData.parents.forEach(parentId => {
// Ensure both parent and child nodes exist in the tree to avoid errors
if (tree[parentId] && tree[nodeId]) {
let edgeColor = "black";
if (dimmedNodes.length > 0 && (!dimmedNodes.includes(parentId) || !dimmedNodes.includes(nodeId))) {
edgeColor = "lightgray";
}
// Highlight edge if both source and target are highlighted/focus
if ((parentId === focusNodeId || highlightedNodes.includes(parentId)) &&
(nodeId === focusNodeId || highlightedNodes.includes(nodeId))) {
edgeColor = "darkgreen"; // Or blue if one is focus
}
dotstring += ` "${parentId}" -> "${nodeId}" [color="${edgeColor}"];\n`;
}
});
}
});
dotstring += '}\n';
return dotstring;
}
nodes = getNode(focus_id)
greyblock = (x) => md`<div style="background-color:#eeeeee; padding-left: 10px; padding-right: 10px; padding-top: 1px; padding-bottom: 1px; border-radius: 8px; width:${Math.min(640, width)}px">${x}</div>`
Purpose-built for displays of data
Observable is your go-to platform for exploring data and creating expressive data visualizations. Use reactive JavaScript notebooks for prototyping and a collaborative canvas for visual data exploration and dashboard creation.
