From d9af04537181bf87373849b0e1856ee8935d2edc Mon Sep 17 00:00:00 2001 From: George Thomas Date: Tue, 29 Aug 2023 14:48:24 +0100 Subject: [PATCH 1/3] refactor: Generalise layout to allow extra per-node padding These values will be used to affect tree layout, without changing the rendering of individual nodes. This is essentially a workaround for the Tidy library not having support for per-edge lengths. Signed-off-by: George Thomas --- src/components/TreeReactFlow/Types.ts | 8 +++++ src/components/TreeReactFlow/layoutTree.ts | 42 ++++++++++++++++------ 2 files changed, 40 insertions(+), 10 deletions(-) diff --git a/src/components/TreeReactFlow/Types.ts b/src/components/TreeReactFlow/Types.ts index 3c2cd6d7..f548d4b9 100644 --- a/src/components/TreeReactFlow/Types.ts +++ b/src/components/TreeReactFlow/Types.ts @@ -134,6 +134,13 @@ export const primerNodeWith = (n: PrimerNode, x: T): PrimerNode => data: { ...n1.data, ...x }, }))(n); +export type Padding = { + top?: number; + bottom?: number; + left?: number; + right?: number; +}; + /** Data corresponding to a node from the backend. * This is not used by special nodes, like term definition names or most parts of type definitions, * but only in places where the backend allows an arbitrarily nested (term or type) expression. @@ -203,6 +210,7 @@ export type PrimerTypeDefConsNodeProps = { export type PrimerCommonNodeProps = { width: number; height: number; + padding?: Padding; selected: boolean; style: "inline" | "corner"; }; diff --git a/src/components/TreeReactFlow/layoutTree.ts b/src/components/TreeReactFlow/layoutTree.ts index 8e51cdcd..d2d2c2d0 100644 --- a/src/components/TreeReactFlow/layoutTree.ts +++ b/src/components/TreeReactFlow/layoutTree.ts @@ -6,7 +6,7 @@ import { import { WasmLayoutType } from "@zxch3n/tidy/wasm_dist"; import { unzip } from "fp-ts/lib/Array"; import { fst, mapFst, mapSnd } from "fp-ts/lib/Tuple"; -import { treeMap, Tree, Positioned } from "./Types"; +import { treeMap, Tree, Positioned, Padding } from "./Types"; export type LayoutParams = { type: WasmLayoutType; @@ -16,7 +16,7 @@ export type LayoutParams = { export const layoutTree = < N extends { id: string; - data: { width: number; height: number }; + data: { width: number; height: number; padding?: Padding }; }, E extends { source: string; @@ -47,18 +47,31 @@ export const layoutTree = < (id) => nodeMap.get(id)! ); const nodes = Array.from(nodeMap.values()).map((n) => n.node); - const minX = Math.min(...nodes.map((n) => n.position.x)); - const minY = Math.min(...nodes.map((n) => n.position.y)); + const minX = Math.min( + ...nodes.map((n) => n.position.x - (n.data.padding?.left || 0)) + ); + const minY = Math.min( + ...nodes.map((n) => n.position.y - (n.data.padding?.top || 0)) + ); const tree = treeMap(treeUnNormalized, (n) => ({ ...n, // Ensure top-left is at (0,0). This makes the result easier to work with. position: { x: n.position.x - minX, y: n.position.y - minY }, })); const width = nodes - ? Math.max(...nodes.map((n) => n.position.x + n.data.width)) - minX + ? Math.max( + ...nodes.map( + (n) => n.position.x + n.data.width + (n.data.padding?.right || 0) + ) + ) - minX : 0; const height = nodes - ? Math.max(...nodes.map((n) => n.position.y + n.data.height)) - minY + ? Math.max( + ...nodes.map( + (n) => + n.position.y + n.data.height + (n.data.padding?.bottom || 0) + ) + ) - minY : 0; return { tree, width, height }; } @@ -84,7 +97,7 @@ type TreeNode = { const makeNodeMap = < N extends { id: string; - data: { width: number; height: number }; + data: { width: number; height: number; padding?: Padding }; }, E extends { source: string; target: string }, >( @@ -129,7 +142,10 @@ const makeNodeMap = < // since we use dummy edges e.g. in order to obtain a more desirable placement of right-children. // Tidy uses numeric IDs, so we must label nodes with ascending integers. // As well as the Tidy tree itself, we also output extra info needed to reconstruct the Primer tree from it. -const primerToTidy = ( +const primerToTidy = < + N extends { data: { width: number; height: number; padding?: Padding } }, + E, +>( t0: Tree ): [TidyNode, NodeInfo[], EdgeInfo[]] => { const nodeInfos: NodeInfo[] = []; @@ -153,8 +169,14 @@ const primerToTidy = ( }); children.forEach(([_, e]) => edgeInfos.push(e)); return { - width: t.node.data.width, - height: t.node.data.height, + width: + t.node.data.width + + (t.node.data.padding?.left || 0) + + (t.node.data.padding?.right || 0), + height: + t.node.data.height + + (t.node.data.padding?.bottom || 0) + + (t.node.data.padding?.top || 0), children: children.map(fst), id: tidyId, // Initial coordinates are unused and immediately overwritten. From 6f717bbf90c9e30d6a46fb91f93d6c77b99b1a25 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Tue, 29 Aug 2023 14:34:42 +0100 Subject: [PATCH 2/3] fix: Add padding to definition name and constructor nodes This avoids overlaps between highlighted nodes and dashed edges. Signed-off-by: George Thomas --- src/components/TreeReactFlow/index.tsx | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/components/TreeReactFlow/index.tsx b/src/components/TreeReactFlow/index.tsx index b0cf2d6d..1e47d1d0 100644 --- a/src/components/TreeReactFlow/index.tsx +++ b/src/components/TreeReactFlow/index.tsx @@ -50,6 +50,7 @@ import { PrimerTypeDefParamNodeProps, PrimerTypeDefNameNodeProps, NodeData, + Padding, } from "./Types"; import { LayoutParams, layoutTree } from "./layoutTree"; import { @@ -100,6 +101,7 @@ type NodeParams = { nodeWidth: number; nodeHeight: number; boxPadding: number; + defNodePadding: Padding; selection?: Selection; level: Level; showIDs: boolean; @@ -137,6 +139,7 @@ export const defaultTreeReactFlowProps: Pick< nodeHeight: 35, boxPadding: 55, defParams: { nameNodeMultipliers: { width: 3, height: 2 } }, + defNodePadding: { bottom: 16 }, layout: { type: WasmLayoutType.Tidy, margins: { child: 28, sibling: 18 }, @@ -853,6 +856,7 @@ const defToTree = async ( contents: { def: def.name }, }), nested: [], + padding: p.defNodePadding, }, type: "primer-def-name", zIndex: 0, @@ -1053,6 +1057,7 @@ const typeDefToTree = async ( }, }, }), + padding: p.defNodePadding, }, zIndex: 0, }, @@ -1084,6 +1089,7 @@ const typeDefToTree = async ( tag: "SelectionTypeDef", contents: { def: def.name }, }), + padding: p.defNodePadding, }, zIndex: 0, }, From ca7b083d888afbbd9799ae344ffcdb698a9e66a1 Mon Sep 17 00:00:00 2001 From: George Thomas Date: Tue, 29 Aug 2023 14:50:48 +0100 Subject: [PATCH 3/3] fix: Add padding to kind nodes This avoids overlaps between siblings. Signed-off-by: George Thomas --- src/components/TreeReactFlow/index.tsx | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/components/TreeReactFlow/index.tsx b/src/components/TreeReactFlow/index.tsx index 1e47d1d0..777d5d75 100644 --- a/src/components/TreeReactFlow/index.tsx +++ b/src/components/TreeReactFlow/index.tsx @@ -680,6 +680,18 @@ const makePrimerNode = async ( ...common, // Square, with same height as other nodes. width: common.height, + ...(flavorSort(flavor) == "kind" + ? { + padding: { + // Since these nodes are rotated, their width, + // as reported to the layout engine, is off by a factor of √2. + // We don't pad vertically since allowing some overlap in the y-axis actually looks better, + // due to the rotation and the fact that all non-leaf kind nodes have precisely two children. + left: (common.height * Math.sqrt(2) - common.height) / 2, + right: (common.height * Math.sqrt(2) - common.height) / 2, + }, + } + : {}), }, zIndex, },