2023-08-16 11:45:05 +03:00
|
|
|
|
import { useCallback, useLayoutEffect, useMemo, useRef, useState } from 'react';
|
2023-08-27 00:19:19 +03:00
|
|
|
|
import { GraphCanvas, GraphCanvasRef, GraphEdge,
|
|
|
|
|
GraphNode, LayoutTypes, Sphere, useSelection
|
2023-08-15 21:22:21 +03:00
|
|
|
|
} from 'reagraph';
|
2023-07-29 23:00:03 +03:00
|
|
|
|
|
2023-08-15 21:22:21 +03:00
|
|
|
|
import ConceptTooltip from '../../components/Common/ConceptTooltip';
|
2023-08-16 00:39:16 +03:00
|
|
|
|
import MiniButton from '../../components/Common/MiniButton';
|
2023-09-14 16:53:38 +03:00
|
|
|
|
import SelectSingle from '../../components/Common/SelectSingle';
|
2023-11-01 14:09:44 +03:00
|
|
|
|
import ConstituentaTooltip from '../../components/Help/ConstituentaTooltip';
|
2023-08-23 18:11:42 +03:00
|
|
|
|
import HelpTermGraph from '../../components/Help/HelpTermGraph';
|
2023-08-16 10:11:22 +03:00
|
|
|
|
import InfoConstituenta from '../../components/Help/InfoConstituenta';
|
2023-10-29 23:24:58 +03:00
|
|
|
|
import { ArrowsFocusIcon, DumpBinIcon, FilterIcon, HelpIcon, LetterAIcon, LetterALinesIcon, PlanetIcon, SmallPlusIcon } from '../../components/Icons';
|
2023-07-29 21:23:18 +03:00
|
|
|
|
import { useRSForm } from '../../context/RSFormContext';
|
2023-07-31 22:38:58 +03:00
|
|
|
|
import { useConceptTheme } from '../../context/ThemeContext';
|
2023-11-01 13:47:49 +03:00
|
|
|
|
import DlgGraphOptions from '../../dialogs/DlgGraphOptions';
|
2023-07-30 00:47:07 +03:00
|
|
|
|
import useLocalStorage from '../../hooks/useLocalStorage';
|
2023-11-01 14:09:44 +03:00
|
|
|
|
import { GraphEditorParams } from '../../models/miscelanious';
|
2023-09-11 20:31:54 +03:00
|
|
|
|
import { CstType, IConstituenta, ICstCreateData } from '../../models/rsform';
|
2023-08-27 15:39:49 +03:00
|
|
|
|
import { graphDarkT, graphLightT, IColorTheme } from '../../utils/color';
|
2023-09-21 14:58:01 +03:00
|
|
|
|
import { colorbgCstClass } from '../../utils/color';
|
|
|
|
|
import { colorbgCstStatus } from '../../utils/color';
|
2023-10-02 23:43:29 +03:00
|
|
|
|
import { prefixes, resources, TIMEOUT_GRAPH_REFRESH } from '../../utils/constants';
|
|
|
|
|
import { Graph } from '../../utils/Graph';
|
2023-09-21 14:58:01 +03:00
|
|
|
|
import { mapLabelColoring } from '../../utils/labels';
|
|
|
|
|
import { mapLableLayout } from '../../utils/labels';
|
2023-10-02 23:43:29 +03:00
|
|
|
|
import { SelectorGraphLayout } from '../../utils/selectors';
|
|
|
|
|
import { SelectorGraphColoring } from '../../utils/selectors';
|
2023-07-29 21:23:18 +03:00
|
|
|
|
|
2023-08-15 21:22:21 +03:00
|
|
|
|
export type ColoringScheme = 'none' | 'status' | 'type';
|
|
|
|
|
const TREE_SIZE_MILESTONE = 50;
|
|
|
|
|
|
2023-08-27 15:39:49 +03:00
|
|
|
|
function getCstNodeColor(cst: IConstituenta, coloringScheme: ColoringScheme, colors: IColorTheme): string {
|
2023-08-15 21:22:21 +03:00
|
|
|
|
if (coloringScheme === 'type') {
|
2023-09-21 14:58:01 +03:00
|
|
|
|
return colorbgCstClass(cst.cst_class, colors);
|
2023-08-15 21:22:21 +03:00
|
|
|
|
}
|
|
|
|
|
if (coloringScheme === 'status') {
|
2023-09-21 14:58:01 +03:00
|
|
|
|
return colorbgCstStatus(cst.status, colors);
|
2023-08-15 21:22:21 +03:00
|
|
|
|
}
|
2023-08-27 15:39:49 +03:00
|
|
|
|
return '';
|
2023-08-16 00:39:16 +03:00
|
|
|
|
}
|
|
|
|
|
|
2023-08-15 21:22:21 +03:00
|
|
|
|
interface EditorTermGraphProps {
|
2023-08-22 22:38:27 +03:00
|
|
|
|
onOpenEdit: (cstID: number) => void
|
2023-08-16 18:32:37 +03:00
|
|
|
|
onCreateCst: (initial: ICstCreateData, skipDialog?: boolean) => void
|
2023-08-22 22:38:27 +03:00
|
|
|
|
onDeleteCst: (selected: number[], callback: (items: number[]) => void) => void
|
2023-08-15 21:22:21 +03:00
|
|
|
|
}
|
|
|
|
|
|
2023-08-16 11:45:05 +03:00
|
|
|
|
function EditorTermGraph({ onOpenEdit, onCreateCst, onDeleteCst }: EditorTermGraphProps) {
|
|
|
|
|
const { schema, isEditable } = useRSForm();
|
2023-08-27 00:19:19 +03:00
|
|
|
|
const { darkMode, colors, noNavigation } = useConceptTheme();
|
2023-08-15 21:22:21 +03:00
|
|
|
|
|
2023-08-08 18:44:30 +03:00
|
|
|
|
const [ layout, setLayout ] = useLocalStorage<LayoutTypes>('graph_layout', 'treeTd2d');
|
2023-09-03 18:26:50 +03:00
|
|
|
|
const [ coloringScheme, setColoringScheme ] = useLocalStorage<ColoringScheme>('graph_coloring', 'type');
|
2023-07-31 22:38:58 +03:00
|
|
|
|
const [ orbit, setOrbit ] = useState(false);
|
2023-08-16 00:39:16 +03:00
|
|
|
|
|
2023-08-03 16:42:49 +03:00
|
|
|
|
const [ noHermits, setNoHermits ] = useLocalStorage('graph_no_hermits', true);
|
2023-10-29 23:24:58 +03:00
|
|
|
|
const [ noTransitive, setNoTransitive ] = useLocalStorage('graph_no_transitive', true);
|
2023-08-16 00:39:16 +03:00
|
|
|
|
const [ noTemplates, setNoTemplates ] = useLocalStorage('graph_no_templates', false);
|
2023-08-16 00:50:27 +03:00
|
|
|
|
const [ noTerms, setNoTerms ] = useLocalStorage('graph_no_terms', false);
|
2023-08-16 00:39:16 +03:00
|
|
|
|
const [ allowBase, setAllowBase ] = useLocalStorage('graph_allow_base', true);
|
|
|
|
|
const [ allowStruct, setAllowStruct ] = useLocalStorage('graph_allow_struct', true);
|
|
|
|
|
const [ allowTerm, setAllowTerm ] = useLocalStorage('graph_allow_term', true);
|
|
|
|
|
const [ allowAxiom, setAllowAxiom ] = useLocalStorage('graph_allow_axiom', true);
|
|
|
|
|
const [ allowFunction, setAllowFunction ] = useLocalStorage('function', true);
|
|
|
|
|
const [ allowPredicate, setAllowPredicate ] = useLocalStorage('graph_allow_predicate', true);
|
|
|
|
|
const [ allowConstant, setAllowConstant ] = useLocalStorage('graph_allow_constant', true);
|
|
|
|
|
const [ allowTheorem, setAllowTheorem ] = useLocalStorage('graph_allow_theorem', true);
|
2023-08-15 21:22:21 +03:00
|
|
|
|
|
|
|
|
|
const [ filtered, setFiltered ] = useState<Graph>(new Graph());
|
2023-08-22 22:38:27 +03:00
|
|
|
|
const [ dismissed, setDismissed ] = useState<number[]>([]);
|
|
|
|
|
const [ selectedDismissed, setSelectedDismissed ] = useState<number[]>([]);
|
2023-07-30 00:47:07 +03:00
|
|
|
|
const graphRef = useRef<GraphCanvasRef | null>(null);
|
2023-08-16 00:39:16 +03:00
|
|
|
|
const [showOptions, setShowOptions] = useState(false);
|
2023-08-16 11:45:05 +03:00
|
|
|
|
const [toggleUpdate, setToggleUpdate] = useState(false);
|
2023-08-15 21:22:21 +03:00
|
|
|
|
|
2023-08-22 22:38:27 +03:00
|
|
|
|
const [hoverID, setHoverID] = useState<number | undefined>(undefined);
|
2023-08-15 21:22:21 +03:00
|
|
|
|
const hoverCst = useMemo(
|
|
|
|
|
() => {
|
2023-08-22 22:38:27 +03:00
|
|
|
|
return schema?.items.find(cst => cst.id === hoverID);
|
2023-08-15 21:22:21 +03:00
|
|
|
|
}, [schema?.items, hoverID]);
|
2023-07-29 23:00:03 +03:00
|
|
|
|
|
2023-08-15 21:22:21 +03:00
|
|
|
|
const is3D = useMemo(() => layout.includes('3d'), [layout]);
|
2023-08-16 00:39:16 +03:00
|
|
|
|
const allowedTypes: CstType[] = useMemo(
|
|
|
|
|
() => {
|
|
|
|
|
const result: CstType[] = [];
|
|
|
|
|
if (allowBase) result.push(CstType.BASE);
|
|
|
|
|
if (allowStruct) result.push(CstType.STRUCTURED);
|
|
|
|
|
if (allowTerm) result.push(CstType.TERM);
|
|
|
|
|
if (allowAxiom) result.push(CstType.AXIOM);
|
|
|
|
|
if (allowFunction) result.push(CstType.FUNCTION);
|
|
|
|
|
if (allowPredicate) result.push(CstType.PREDICATE);
|
|
|
|
|
if (allowConstant) result.push(CstType.CONSTANT);
|
|
|
|
|
if (allowTheorem) result.push(CstType.THEOREM);
|
|
|
|
|
return result;
|
|
|
|
|
}, [allowBase, allowStruct, allowTerm, allowAxiom, allowFunction, allowPredicate, allowConstant, allowTheorem]);
|
2023-08-15 21:22:21 +03:00
|
|
|
|
|
2023-08-16 11:45:05 +03:00
|
|
|
|
useLayoutEffect(
|
2023-08-15 21:22:21 +03:00
|
|
|
|
() => {
|
2023-08-03 16:42:49 +03:00
|
|
|
|
if (!schema) {
|
|
|
|
|
setFiltered(new Graph());
|
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
const graph = schema.graph.clone();
|
|
|
|
|
if (noHermits) {
|
|
|
|
|
graph.removeIsolated();
|
|
|
|
|
}
|
|
|
|
|
if (noTransitive) {
|
|
|
|
|
graph.transitiveReduction();
|
|
|
|
|
}
|
2023-08-16 00:39:16 +03:00
|
|
|
|
if (noTemplates) {
|
|
|
|
|
schema.items.forEach(cst => {
|
2023-08-29 15:17:16 +03:00
|
|
|
|
if (cst.is_template) {
|
2023-08-16 00:39:16 +03:00
|
|
|
|
graph.foldNode(cst.id);
|
|
|
|
|
}
|
|
|
|
|
});
|
|
|
|
|
}
|
|
|
|
|
if (allowedTypes.length < Object.values(CstType).length) {
|
|
|
|
|
schema.items.forEach(cst => {
|
2023-08-29 15:17:16 +03:00
|
|
|
|
if (!allowedTypes.includes(cst.cst_type)) {
|
2023-08-16 00:39:16 +03:00
|
|
|
|
graph.foldNode(cst.id);
|
|
|
|
|
}
|
|
|
|
|
});
|
|
|
|
|
}
|
2023-08-22 22:38:27 +03:00
|
|
|
|
const newDismissed: number[] = [];
|
2023-08-15 21:22:21 +03:00
|
|
|
|
schema.items.forEach(cst => {
|
|
|
|
|
if (!graph.nodes.has(cst.id)) {
|
|
|
|
|
newDismissed.push(cst.id);
|
|
|
|
|
}
|
|
|
|
|
});
|
2023-08-03 16:42:49 +03:00
|
|
|
|
setFiltered(graph);
|
2023-08-15 21:22:21 +03:00
|
|
|
|
setDismissed(newDismissed);
|
|
|
|
|
setSelectedDismissed([]);
|
|
|
|
|
setHoverID(undefined);
|
2023-08-16 11:45:05 +03:00
|
|
|
|
}, [schema, noHermits, noTransitive, noTemplates, allowedTypes, toggleUpdate]);
|
2023-08-03 16:42:49 +03:00
|
|
|
|
|
2023-08-22 22:38:27 +03:00
|
|
|
|
function toggleDismissed(cstID: number) {
|
2023-08-15 21:22:21 +03:00
|
|
|
|
setSelectedDismissed(prev => {
|
2023-08-22 20:29:07 +03:00
|
|
|
|
const index = prev.findIndex(id => cstID === id);
|
2023-08-15 21:22:21 +03:00
|
|
|
|
if (index !== -1) {
|
|
|
|
|
prev.splice(index, 1);
|
|
|
|
|
} else {
|
|
|
|
|
prev.push(cstID);
|
|
|
|
|
}
|
|
|
|
|
return [... prev];
|
|
|
|
|
});
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
const nodes: GraphNode[] = useMemo(
|
|
|
|
|
() => {
|
2023-08-03 16:42:49 +03:00
|
|
|
|
const result: GraphNode[] = [];
|
|
|
|
|
if (!schema) {
|
|
|
|
|
return result;
|
|
|
|
|
}
|
|
|
|
|
filtered.nodes.forEach(node => {
|
|
|
|
|
const cst = schema.items.find(cst => cst.id === node.id);
|
|
|
|
|
if (cst) {
|
|
|
|
|
result.push({
|
2023-08-22 22:38:27 +03:00
|
|
|
|
id: String(node.id),
|
2023-08-27 15:39:49 +03:00
|
|
|
|
fill: getCstNodeColor(cst, coloringScheme, colors),
|
2023-08-29 15:17:16 +03:00
|
|
|
|
label: cst.term_resolved && !noTerms ? `${cst.alias}: ${cst.term_resolved}` : cst.alias
|
2023-08-03 16:42:49 +03:00
|
|
|
|
});
|
|
|
|
|
}
|
|
|
|
|
});
|
|
|
|
|
return result;
|
2023-08-27 15:39:49 +03:00
|
|
|
|
}, [schema, coloringScheme, filtered.nodes, noTerms, colors]);
|
2023-07-29 21:23:18 +03:00
|
|
|
|
|
2023-08-15 21:22:21 +03:00
|
|
|
|
const edges: GraphEdge[] = useMemo(
|
|
|
|
|
() => {
|
2023-07-29 23:00:03 +03:00
|
|
|
|
const result: GraphEdge[] = [];
|
|
|
|
|
let edgeID = 1;
|
2023-08-03 16:42:49 +03:00
|
|
|
|
filtered.nodes.forEach(source => {
|
2023-08-02 18:24:17 +03:00
|
|
|
|
source.outputs.forEach(target => {
|
2023-07-29 23:00:03 +03:00
|
|
|
|
result.push({
|
|
|
|
|
id: String(edgeID),
|
2023-08-22 22:38:27 +03:00
|
|
|
|
source: String(source.id),
|
|
|
|
|
target: String(target)
|
2023-07-29 23:00:03 +03:00
|
|
|
|
});
|
|
|
|
|
edgeID += 1;
|
|
|
|
|
});
|
|
|
|
|
});
|
|
|
|
|
return result;
|
2023-08-03 16:42:49 +03:00
|
|
|
|
}, [filtered.nodes]);
|
2023-08-15 21:22:21 +03:00
|
|
|
|
|
2023-07-30 00:47:07 +03:00
|
|
|
|
const {
|
|
|
|
|
selections, actives,
|
|
|
|
|
onNodeClick,
|
2023-08-16 11:45:05 +03:00
|
|
|
|
clearSelections,
|
2023-07-30 00:47:07 +03:00
|
|
|
|
onCanvasClick,
|
|
|
|
|
onNodePointerOver,
|
|
|
|
|
onNodePointerOut
|
|
|
|
|
} = useSelection({
|
|
|
|
|
ref: graphRef,
|
|
|
|
|
nodes,
|
|
|
|
|
edges,
|
2023-07-31 22:38:58 +03:00
|
|
|
|
type: 'multi', // 'single' | 'multi' | 'multiModifier'
|
2023-08-16 00:50:27 +03:00
|
|
|
|
pathSelectionType: 'out',
|
|
|
|
|
pathHoverType: 'all',
|
2023-07-31 22:38:58 +03:00
|
|
|
|
focusOnSelect: false
|
2023-07-30 00:47:07 +03:00
|
|
|
|
});
|
|
|
|
|
|
2023-08-22 22:38:27 +03:00
|
|
|
|
const allSelected: number[] = useMemo(
|
2023-08-16 11:45:05 +03:00
|
|
|
|
() => {
|
2023-08-22 22:38:27 +03:00
|
|
|
|
return [ ... selectedDismissed, ... selections.map(id => Number(id))];
|
2023-08-16 11:45:05 +03:00
|
|
|
|
}, [selectedDismissed, selections]);
|
|
|
|
|
const nothingSelected = useMemo(() => allSelected.length === 0, [allSelected]);
|
2023-08-16 10:46:22 +03:00
|
|
|
|
|
2023-09-08 02:15:20 +03:00
|
|
|
|
const handleResetViewpoint = useCallback(
|
2023-08-15 21:22:21 +03:00
|
|
|
|
() => {
|
2023-09-08 02:15:20 +03:00
|
|
|
|
graphRef.current?.resetControls(true);
|
2023-08-15 21:22:21 +03:00
|
|
|
|
graphRef.current?.centerGraph();
|
|
|
|
|
}, []);
|
|
|
|
|
|
|
|
|
|
const handleHoverIn = useCallback(
|
|
|
|
|
(node: GraphNode) => {
|
2023-08-22 22:38:27 +03:00
|
|
|
|
setHoverID(Number(node.id));
|
2023-08-15 21:22:21 +03:00
|
|
|
|
if (onNodePointerOver) onNodePointerOver(node);
|
|
|
|
|
}, [onNodePointerOver]);
|
|
|
|
|
|
|
|
|
|
const handleHoverOut = useCallback(
|
|
|
|
|
(node: GraphNode) => {
|
|
|
|
|
setHoverID(undefined);
|
|
|
|
|
if (onNodePointerOut) onNodePointerOut(node);
|
|
|
|
|
}, [onNodePointerOut]);
|
|
|
|
|
|
|
|
|
|
const handleNodeClick = useCallback(
|
|
|
|
|
(node: GraphNode) => {
|
|
|
|
|
if (selections.includes(node.id)) {
|
2023-08-22 22:38:27 +03:00
|
|
|
|
onOpenEdit(Number(node.id));
|
2023-08-15 21:22:21 +03:00
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
if (onNodeClick) onNodeClick(node);
|
|
|
|
|
}, [onNodeClick, selections, onOpenEdit]);
|
|
|
|
|
|
2023-08-16 10:46:22 +03:00
|
|
|
|
const handleCanvasClick = useCallback(
|
|
|
|
|
(event: MouseEvent) => {
|
|
|
|
|
setSelectedDismissed([]);
|
|
|
|
|
if (onCanvasClick) onCanvasClick(event);
|
|
|
|
|
}, [onCanvasClick]);
|
|
|
|
|
|
2023-08-16 11:45:05 +03:00
|
|
|
|
// Implement hotkeys for editing
|
|
|
|
|
function handleKeyDown(event: React.KeyboardEvent<HTMLDivElement>) {
|
|
|
|
|
if (!isEditable) {
|
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
if (event.key === 'Delete' && allSelected.length > 0) {
|
|
|
|
|
event.preventDefault();
|
|
|
|
|
handleDeleteCst();
|
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
function handleCreateCst() {
|
|
|
|
|
if (!schema) {
|
|
|
|
|
return;
|
|
|
|
|
}
|
2023-08-16 18:32:37 +03:00
|
|
|
|
const data: ICstCreateData = {
|
|
|
|
|
insert_after: null,
|
2023-08-22 20:29:07 +03:00
|
|
|
|
cst_type: allSelected.length === 0 ? CstType.BASE: CstType.TERM,
|
2023-08-16 18:32:37 +03:00
|
|
|
|
alias: '',
|
|
|
|
|
term_raw: '',
|
2023-08-22 20:29:07 +03:00
|
|
|
|
definition_formal: allSelected.map(id => schema.items.find(cst => cst.id === id)!.alias).join(' '),
|
2023-08-16 18:32:37 +03:00
|
|
|
|
definition_raw: '',
|
|
|
|
|
convention: '',
|
2023-10-25 21:21:43 +03:00
|
|
|
|
term_forms: []
|
2023-08-16 18:32:37 +03:00
|
|
|
|
};
|
|
|
|
|
onCreateCst(data);
|
2023-08-16 11:45:05 +03:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
function handleDeleteCst() {
|
|
|
|
|
if (!schema) {
|
|
|
|
|
return;
|
|
|
|
|
}
|
2023-08-22 20:29:07 +03:00
|
|
|
|
onDeleteCst(allSelected, () => {
|
2023-08-16 11:45:05 +03:00
|
|
|
|
clearSelections();
|
|
|
|
|
setDismissed([]);
|
|
|
|
|
setSelectedDismissed([]);
|
|
|
|
|
setToggleUpdate(prev => !prev);
|
|
|
|
|
});
|
|
|
|
|
}
|
|
|
|
|
|
2023-09-08 02:15:20 +03:00
|
|
|
|
function handleChangeLayout(newLayout: LayoutTypes) {
|
|
|
|
|
if (newLayout === layout) {
|
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
setLayout(newLayout);
|
|
|
|
|
setTimeout(() => {
|
|
|
|
|
handleResetViewpoint();
|
|
|
|
|
}, TIMEOUT_GRAPH_REFRESH);
|
|
|
|
|
}
|
|
|
|
|
|
2023-08-16 00:39:16 +03:00
|
|
|
|
function getOptions() {
|
|
|
|
|
return {
|
|
|
|
|
noHermits: noHermits,
|
|
|
|
|
noTemplates: noTemplates,
|
|
|
|
|
noTransitive: noTransitive,
|
2023-08-16 00:50:27 +03:00
|
|
|
|
noTerms: noTerms,
|
2023-08-16 00:39:16 +03:00
|
|
|
|
|
|
|
|
|
allowBase: allowBase,
|
|
|
|
|
allowStruct: allowStruct,
|
|
|
|
|
allowTerm: allowTerm,
|
|
|
|
|
allowAxiom: allowAxiom,
|
|
|
|
|
allowFunction: allowFunction,
|
|
|
|
|
allowPredicate: allowPredicate,
|
|
|
|
|
allowConstant: allowConstant,
|
|
|
|
|
allowTheorem: allowTheorem
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
const handleChangeOptions = useCallback(
|
|
|
|
|
(params: GraphEditorParams) => {
|
|
|
|
|
setNoHermits(params.noHermits);
|
|
|
|
|
setNoTransitive(params.noTransitive);
|
|
|
|
|
setNoTemplates(params.noTemplates);
|
2023-08-16 00:50:27 +03:00
|
|
|
|
setNoTerms(params.noTerms);
|
2023-08-16 00:39:16 +03:00
|
|
|
|
|
|
|
|
|
setAllowBase(params.allowBase);
|
|
|
|
|
setAllowStruct(params.allowStruct);
|
|
|
|
|
setAllowTerm(params.allowTerm);
|
|
|
|
|
setAllowAxiom(params.allowAxiom);
|
|
|
|
|
setAllowFunction(params.allowFunction);
|
|
|
|
|
setAllowPredicate(params.allowPredicate);
|
|
|
|
|
setAllowConstant(params.allowConstant);
|
|
|
|
|
setAllowTheorem(params.allowTheorem);
|
|
|
|
|
}, [setNoHermits, setNoTransitive, setNoTemplates,
|
|
|
|
|
setAllowBase, setAllowStruct, setAllowTerm, setAllowAxiom, setAllowFunction,
|
2023-08-16 00:50:27 +03:00
|
|
|
|
setAllowPredicate, setAllowConstant, setAllowTheorem, setNoTerms]);
|
2023-08-16 00:39:16 +03:00
|
|
|
|
|
2023-08-15 21:22:21 +03:00
|
|
|
|
const canvasWidth = useMemo(
|
|
|
|
|
() => {
|
2023-10-29 23:24:58 +03:00
|
|
|
|
return 'calc(100vw - 1.1rem)';
|
2023-08-15 21:22:21 +03:00
|
|
|
|
}, []);
|
|
|
|
|
|
|
|
|
|
const canvasHeight = useMemo(
|
|
|
|
|
() => {
|
|
|
|
|
return !noNavigation ?
|
2023-09-01 00:39:28 +03:00
|
|
|
|
'calc(100vh - 9.8rem - 4px)'
|
|
|
|
|
: 'calc(100vh - 3rem - 4px)';
|
2023-08-15 21:22:21 +03:00
|
|
|
|
}, [noNavigation]);
|
2023-08-04 13:26:51 +03:00
|
|
|
|
|
2023-10-16 01:22:08 +03:00
|
|
|
|
const dismissedHeight = useMemo(
|
|
|
|
|
() => {
|
|
|
|
|
return !noNavigation ?
|
|
|
|
|
'calc(100vh - 28rem - 4px)'
|
|
|
|
|
: 'calc(100vh - 22.2rem - 4px)';
|
|
|
|
|
}, [noNavigation]);
|
|
|
|
|
|
2023-08-15 21:22:21 +03:00
|
|
|
|
const dismissedStyle = useCallback(
|
2023-08-22 22:38:27 +03:00
|
|
|
|
(cstID: number) => {
|
2023-08-15 21:22:21 +03:00
|
|
|
|
return selectedDismissed.includes(cstID) ? {outlineWidth: '2px', outlineStyle: 'solid'}: {};
|
|
|
|
|
}, [selectedDismissed]);
|
|
|
|
|
|
2023-10-16 01:22:08 +03:00
|
|
|
|
return (<>
|
2023-08-16 00:39:16 +03:00
|
|
|
|
{showOptions &&
|
|
|
|
|
<DlgGraphOptions
|
|
|
|
|
hideWindow={() => setShowOptions(false)}
|
|
|
|
|
initial={getOptions()}
|
|
|
|
|
onConfirm={handleChangeOptions}
|
|
|
|
|
/>}
|
2023-10-16 01:22:08 +03:00
|
|
|
|
|
2023-10-29 23:24:58 +03:00
|
|
|
|
{ allSelected.length > 0 &&
|
|
|
|
|
<div className='relative w-full z-pop'>
|
2023-11-01 13:47:49 +03:00
|
|
|
|
<div className='absolute top-0 left-0 px-2 select-none whitespace-nowrap small-caps clr-app'>
|
2023-10-29 23:24:58 +03:00
|
|
|
|
Выбор {allSelected.length} из {schema?.stats?.count_all ?? 0}
|
|
|
|
|
</div>
|
|
|
|
|
</div>}
|
|
|
|
|
|
2023-10-16 01:22:08 +03:00
|
|
|
|
<div className='relative w-full z-pop'>
|
2023-10-23 18:22:55 +03:00
|
|
|
|
<div className='absolute right-0 flex items-start justify-center w-full top-1'>
|
2023-10-29 23:24:58 +03:00
|
|
|
|
<MiniButton
|
|
|
|
|
tooltip='Настройки фильтрации узлов и связей'
|
|
|
|
|
icon={<FilterIcon color='text-primary' size={5}/>}
|
|
|
|
|
onClick={() => setShowOptions(true)}
|
|
|
|
|
/>
|
|
|
|
|
<MiniButton
|
|
|
|
|
tooltip={ !noTerms ? 'Скрыть текст' : 'Отобразить текст' }
|
|
|
|
|
icon={ !noTerms ? <LetterALinesIcon color='text-success' size={5}/> : <LetterAIcon color='text-primary' size={5}/> }
|
|
|
|
|
onClick={() => setNoTerms(prev => !prev)}
|
|
|
|
|
/>
|
2023-10-16 01:22:08 +03:00
|
|
|
|
<MiniButton
|
|
|
|
|
tooltip='Новая конституента'
|
|
|
|
|
icon={<SmallPlusIcon color={isEditable ? 'text-success': ''} size={5}/>}
|
|
|
|
|
disabled={!isEditable}
|
|
|
|
|
onClick={handleCreateCst}
|
|
|
|
|
/>
|
|
|
|
|
<MiniButton
|
|
|
|
|
tooltip='Удалить выбранные'
|
|
|
|
|
icon={<DumpBinIcon color={isEditable && !nothingSelected ? 'text-warning' : ''} size={5}/>}
|
|
|
|
|
disabled={!isEditable || nothingSelected}
|
|
|
|
|
onClick={handleDeleteCst}
|
|
|
|
|
/>
|
|
|
|
|
<MiniButton
|
2023-10-29 23:24:58 +03:00
|
|
|
|
icon={<ArrowsFocusIcon color='text-primary' size={5} />}
|
2023-10-16 01:22:08 +03:00
|
|
|
|
tooltip='Восстановить камеру'
|
|
|
|
|
onClick={handleResetViewpoint}
|
|
|
|
|
/>
|
2023-10-29 23:24:58 +03:00
|
|
|
|
<MiniButton
|
|
|
|
|
icon={<PlanetIcon color={ !is3D ? '' : orbit ? 'text-success' : 'text-primary'} size={5} />}
|
|
|
|
|
tooltip='Анимация вращения'
|
|
|
|
|
disabled={!is3D}
|
|
|
|
|
onClick={() => setOrbit(prev => !prev) }
|
|
|
|
|
/>
|
2023-10-16 01:22:08 +03:00
|
|
|
|
<div className='px-1 py-1' id='items-graph-help' >
|
|
|
|
|
<HelpIcon color='text-primary' size={5} />
|
|
|
|
|
</div>
|
2023-10-29 23:24:58 +03:00
|
|
|
|
<ConceptTooltip anchorSelect='#items-graph-help'>
|
|
|
|
|
<div className='text-sm max-w-[calc(100vw-20rem)] z-tooltip'>
|
|
|
|
|
<HelpTermGraph />
|
|
|
|
|
</div>
|
|
|
|
|
</ConceptTooltip>
|
2023-10-16 01:22:08 +03:00
|
|
|
|
</div>
|
|
|
|
|
</div>
|
|
|
|
|
|
2023-10-29 23:24:58 +03:00
|
|
|
|
{hoverCst &&
|
|
|
|
|
<div className='relative'>
|
|
|
|
|
<InfoConstituenta
|
|
|
|
|
data={hoverCst}
|
|
|
|
|
className='absolute top-[1.6rem] left-[2.6rem] z-tooltip w-[25rem] min-h-[11rem] shadow-md overflow-y-auto border h-fit clr-app px-3'
|
|
|
|
|
/>
|
|
|
|
|
</div>}
|
|
|
|
|
|
|
|
|
|
<div className='relative z-pop'>
|
|
|
|
|
<div className='absolute top-0 left-0 flex flex-col max-w-[13.5rem] min-w-[13.5rem]'>
|
|
|
|
|
<div className='flex flex-col px-2 pb-2 mt-8 text-sm select-none h-fit'>
|
|
|
|
|
<div className='flex items-center w-full gap-1 text-sm'>
|
2023-10-16 01:22:08 +03:00
|
|
|
|
<SelectSingle
|
|
|
|
|
options={SelectorGraphColoring}
|
|
|
|
|
isSearchable={false}
|
|
|
|
|
placeholder='Выберите цвет'
|
|
|
|
|
value={coloringScheme ? { value: coloringScheme, label: mapLabelColoring.get(coloringScheme) } : null}
|
|
|
|
|
onChange={data => setColoringScheme(data?.value ?? SelectorGraphColoring[0].value)}
|
2023-09-15 23:29:52 +03:00
|
|
|
|
/>
|
2023-08-16 11:45:05 +03:00
|
|
|
|
</div>
|
2023-09-14 16:53:38 +03:00
|
|
|
|
<SelectSingle
|
2023-10-16 01:22:08 +03:00
|
|
|
|
className='w-full mt-1'
|
|
|
|
|
options={SelectorGraphLayout}
|
2023-09-08 02:15:20 +03:00
|
|
|
|
isSearchable={false}
|
2023-10-16 01:22:08 +03:00
|
|
|
|
placeholder='Способ расположения'
|
|
|
|
|
value={layout ? { value: layout, label: mapLableLayout.get(layout) } : null}
|
|
|
|
|
onChange={data => handleChangeLayout(data?.value ?? SelectorGraphLayout[0].value)}
|
2023-08-03 16:42:49 +03:00
|
|
|
|
/>
|
|
|
|
|
</div>
|
2023-10-14 21:17:21 +03:00
|
|
|
|
{dismissed.length > 0 &&
|
2023-10-29 23:24:58 +03:00
|
|
|
|
<div className='flex flex-col text-sm ml-2 border clr-app max-w-[12.5rem] min-w-[12.5rem]'>
|
2023-10-18 19:31:11 +03:00
|
|
|
|
<p className='py-2 text-center'><b>Скрытые конституенты</b></p>
|
|
|
|
|
<div className='flex flex-wrap justify-center gap-2 pb-2 overflow-y-auto' style={{maxHeight: dismissedHeight}}>
|
2023-08-15 21:22:21 +03:00
|
|
|
|
{dismissed.map(cstID => {
|
|
|
|
|
const cst = schema!.items.find(cst => cst.id === cstID)!;
|
2023-08-16 00:39:16 +03:00
|
|
|
|
const adjustedColoring = coloringScheme === 'none' ? 'status': coloringScheme;
|
2023-08-15 21:22:21 +03:00
|
|
|
|
return (<>
|
|
|
|
|
<div
|
|
|
|
|
key={`${cst.alias}`}
|
|
|
|
|
id={`${prefixes.cst_list}${cst.alias}`}
|
2023-10-16 01:22:08 +03:00
|
|
|
|
className='w-fit min-w-[3rem] rounded-md text-center cursor-pointer select-none'
|
2023-08-27 00:19:19 +03:00
|
|
|
|
style={{
|
2023-08-27 15:39:49 +03:00
|
|
|
|
backgroundColor: getCstNodeColor(cst, adjustedColoring, colors),
|
2023-08-27 00:19:19 +03:00
|
|
|
|
...dismissedStyle(cstID)
|
|
|
|
|
}}
|
2023-08-15 21:22:21 +03:00
|
|
|
|
onClick={() => toggleDismissed(cstID)}
|
|
|
|
|
onDoubleClick={() => onOpenEdit(cstID)}
|
|
|
|
|
>
|
|
|
|
|
{cst.alias}
|
|
|
|
|
</div>
|
|
|
|
|
<ConstituentaTooltip
|
|
|
|
|
data={cst}
|
|
|
|
|
anchor={`#${prefixes.cst_list}${cst.alias}`}
|
|
|
|
|
/>
|
|
|
|
|
</>);
|
|
|
|
|
})}
|
|
|
|
|
</div>
|
2023-10-14 21:17:21 +03:00
|
|
|
|
</div>}
|
2023-10-29 23:24:58 +03:00
|
|
|
|
</div>
|
|
|
|
|
</div>
|
|
|
|
|
|
2023-11-01 13:47:49 +03:00
|
|
|
|
<div className='w-full h-full overflow-auto outline-none' tabIndex={0} onKeyDown={handleKeyDown}>
|
2023-08-15 21:22:21 +03:00
|
|
|
|
<div
|
2023-08-27 00:19:19 +03:00
|
|
|
|
className='relative'
|
2023-10-13 23:24:46 +03:00
|
|
|
|
style={{width: canvasWidth, height: canvasHeight}}
|
2023-08-15 21:22:21 +03:00
|
|
|
|
>
|
2023-07-31 22:38:58 +03:00
|
|
|
|
<GraphCanvas
|
|
|
|
|
draggable
|
|
|
|
|
ref={graphRef}
|
|
|
|
|
nodes={nodes}
|
|
|
|
|
edges={edges}
|
|
|
|
|
layoutType={layout}
|
|
|
|
|
selections={selections}
|
|
|
|
|
actives={actives}
|
2023-08-15 21:22:21 +03:00
|
|
|
|
onNodeClick={handleNodeClick}
|
2023-08-16 10:46:22 +03:00
|
|
|
|
onCanvasClick={handleCanvasClick}
|
2023-08-15 21:22:21 +03:00
|
|
|
|
onNodePointerOver={handleHoverIn}
|
|
|
|
|
onNodePointerOut={handleHoverOut}
|
|
|
|
|
cameraMode={ orbit ? 'orbit' : is3D ? 'rotate' : 'pan'}
|
|
|
|
|
layoutOverrides={
|
2023-08-16 00:39:16 +03:00
|
|
|
|
layout.includes('tree') ? { nodeLevelRatio: filtered.nodes.size < TREE_SIZE_MILESTONE ? 3 : 1 }
|
2023-08-15 21:22:21 +03:00
|
|
|
|
: undefined
|
|
|
|
|
}
|
2023-07-31 22:38:58 +03:00
|
|
|
|
labelFontUrl={resources.graph_font}
|
2023-08-27 15:39:49 +03:00
|
|
|
|
theme={darkMode ? graphDarkT : graphLightT}
|
2023-08-03 16:42:49 +03:00
|
|
|
|
renderNode={({ node, ...rest }) => (
|
|
|
|
|
<Sphere {...rest} node={node} />
|
|
|
|
|
)}
|
2023-07-29 23:00:03 +03:00
|
|
|
|
/>
|
2023-07-29 21:23:18 +03:00
|
|
|
|
</div>
|
2023-10-16 01:22:08 +03:00
|
|
|
|
</div></>);
|
2023-07-29 21:23:18 +03:00
|
|
|
|
}
|
|
|
|
|
|
2023-07-29 23:00:03 +03:00
|
|
|
|
|
2023-07-29 21:23:18 +03:00
|
|
|
|
export default EditorTermGraph;
|