30:T1083,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; }31:T555,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; }32:T7be,// 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; }33:T774,// 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`

No data loaded for ${focus_id}.

`; } else { return html`

Select a theorem to display its graph.

`; } } // 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

`; 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 = `

No data loaded for ${currentFocusId}. It might be fetching or an error occurred.

`; } else { container.innerHTML = `

Select a theorem to display its dependency graph.

`; } 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 = `

Error preparing graph data: ${e.message}. Check console.

`; return container; } if (cytoscapeElements.filter(el => el.group === 'nodes').length === 0 && Object.keys(raw_graph_data).length > 0) { container.innerHTML = `

Data loaded for ${currentFocusId}, but no visualizable nodes were generated. Check transformation logic.

`; 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 = `

Cytoscape Error: ${e.message}. Check console.

`; } return container; // Return the container, now populated by Cytoscape }35:Td93,// 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; }36:[] 2e:{"title":"Bourbaki 2.0","cells":[{"id":0,"value":"# Bourbaki 2.0","pinned":false,"hidden":false,"mode":"md"},{"id":609,"value":"$${Object.keys(directories).length - Object.keys(thm_ids).length} definitions, ${Object.keys(thm_ids).length} theorems","pinned":false,"hidden":false,"mode":"md"},{"id":391,"value":"dot`${digraph(nodes)}`","pinned":false,"hidden":false,"mode":"ojs"},{"id":146,"value":"greyblock(parseMD(thm))","pinned":false,"hidden":false,"mode":"ojs"},{"id":203,"value":"viewof focus_id = Inputs.select(thm_ids, {label: \"Select theorem\", value: \"S8P9UI0H\"})","pinned":false,"hidden":false,"mode":"ojs"},{"id":281,"value":"viewof statement = Inputs.radio(Object.keys(data['statements']), {label: \"Select statement\", value: focus_id + \"_1\"})","pinned":false,"hidden":false,"mode":"ojs"},{"id":227,"value":"View and edit on GitHub","pinned":false,"hidden":false,"mode":"html"},{"id":238,"value":"viewof proof = Inputs.radio(Object.keys(data['proofs']), {label: \"Select proof\", value: focus_id + \"_a\"})","pinned":false,"hidden":false,"mode":"ojs"},{"id":248,"value":"parseMD(\"*Proof.* \" + pf)","pinned":false,"hidden":false,"mode":"ojs"},{"id":545,"value":"url = 'https://raw.githubusercontent.com/neobourbaki/Library/main/database/'","pinned":false,"hidden":false,"mode":"ojs"},{"id":618,"value":"url2 = \"https://www.github.com/neobourbaki/Library/tree/main/database/\"","pinned":true,"hidden":false,"mode":"ojs"},{"id":593,"value":"directories = fetch('https://api.github.com/repos/neobourbaki/Library/contents/database')\n .then(response => response.json()).then(data => data.filter(item => item.type === 'dir'))","pinned":false,"hidden":false,"mode":"ojs"},{"id":676,"value":"GITHUB_REPO_API_URL = 'https://api.github.com/repos/neobourbaki/Library/contents/database'","pinned":true,"hidden":false,"mode":"ojs"},{"id":196,"value":"available_ids_data = fetch(GITHUB_REPO_API_URL)\n .then(response => {\n if (!response.ok) throw new Error(`GitHub API error: ${response.status}`);\n return response.json();\n })\n .then(data => {\n if (!Array.isArray(data)) throw new Error(\"GitHub API did not return an array for directory contents.\");\n return data.filter(item => item && item.type === 'dir' && item.name);\n })\n .catch(err => {\n console.error(\"Error fetching directory listing:\", err);\n return []; // Return empty array on error\n });","pinned":false,"hidden":false,"mode":"ojs"},{"id":678,"value":"thm_ids = available_ids_data.filter(item => item.name[0] && item.name[0].match(/[A-Z]/)).map(item => item.name)","pinned":true,"hidden":false,"mode":"ojs"},{"id":5,"value":"data = fetch(url + focus_id + \"/\" + focus_id + \".json\")\n .then(response => response.json())","pinned":false,"hidden":false,"mode":"ojs"},{"id":62,"value":"thm = {\n let thm_id = data[\"id\"]\n if (thm_id + \"_1\" in data['statements']) {\n let response = await fetch(url + focus_id + \"/\" + statement + \".md\");\n return response.text();\n }\n return \"not found\";\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":259,"value":"pf = fetch(url + focus_id + \"/\" + proof +\".md\").then(response=>response.text()) || \"\"","pinned":false,"hidden":false,"mode":"ojs"},{"id":77,"value":"function parseMD(content) {\n try {\n let processed = content.replace(/\\\\\\\\/g, '\\\\')\n .replace(/\\$\\$(.*?)\\$\\$/gs, (match, p1) => '

${tex.block`' + p1 + '`}

')\n .replace(/\\$(.*?)\\$/g, (match, p1) => '${tex`' + p1 + '`}');\n return new Function('tex', 'md', 'return md`' + processed + '`')(tex, md);\n } catch (error) {\n return md`>\\`\\`\\`${error}\\`\\`\\`\\n\\n${content}`;\n };\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":460,"value":"function nodeType(id) {\n if (/^[0-9][0-9A-Z]{7}$/.test(id)) return 'def';\n if (/^[A-Z][0-9A-Z]{7}$/.test(id)) return 'thm';\n return null;\n}","pinned":true,"hidden":false,"mode":"ojs"},{"id":299,"value":"$30","pinned":true,"hidden":false,"mode":"ojs"},{"id":694,"value":"raw_graph_data = {\n // This cell will re-run whenever focus_id changes.\n if (!focus_id) {\n // console.log(\"No focus_id selected, returning empty graph data.\");\n return {}; // Return empty object if no focus_id\n }\n // Show a temporary message while fetching. Observable handles this well for async cells.\n // The cell's value will be a Promise that resolves to the tree.\n // console.log(`Fetching graph data starting from: ${focus_id}`);\n return getNode(focus_id, {}, 15, focus_id); // Pass focus_id as initial label too\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":578,"value":"$31","pinned":true,"hidden":false,"mode":"ojs"},{"id":698,"value":"$32","pinned":true,"hidden":false,"mode":"ojs"},{"id":703,"value":"$33","pinned":true,"hidden":false,"mode":"ojs"},{"id":700,"value":"$34","pinned":true,"hidden":false,"mode":"ojs"},{"id":387,"value":"$35","pinned":true,"hidden":false,"mode":"ojs"},{"id":303,"value":"nodes = getNode(focus_id)","pinned":true,"hidden":false,"mode":"ojs"},{"id":637,"value":"## Imports","pinned":false,"hidden":false,"mode":"md"},{"id":657,"value":"cytoscape = {\n // Using a specific version for stability\n const cy = await require(\"cytoscape@3.28.1\");\n if (!cy || typeof cy !== 'function') {\n throw new Error(\"Cytoscape library failed to load correctly.\");\n }\n // If you later want to add extensions like 'dagre', you'd do cy.use(extension) here.\n return cy;\n}","pinned":false,"hidden":false,"mode":"ojs"},{"id":96,"value":"greyblock = (x) => md`

${x}

`","pinned":false,"hidden":true,"mode":"ojs"}],"files":"$W36","stdlib":"1","titling":"auto"}