From 3f0a52ab5feb79c682dfcb0cc2b46a1d33f2b81a Mon Sep 17 00:00:00 2001 From: Joe Krystowski Date: Sun, 8 Oct 2023 17:55:48 -0400 Subject: [PATCH 01/35] refactor graphs --- .../ExistentialGraph.js} | 54 ++++++++++++++----- .../{scripts => existential-graph}/Sheet.js | 4 +- .../shapes}/Atomic.js | 0 .../shapes}/Cut.js | 0 4 files changed, 44 insertions(+), 14 deletions(-) rename client/src/{scripts/Paper.js => existential-graph/ExistentialGraph.js} (91%) rename client/src/{scripts => existential-graph}/Sheet.js (99%) rename client/src/{scripts => existential-graph/shapes}/Atomic.js (100%) rename client/src/{scripts => existential-graph/shapes}/Cut.js (100%) diff --git a/client/src/scripts/Paper.js b/client/src/existential-graph/ExistentialGraph.js similarity index 91% rename from client/src/scripts/Paper.js rename to client/src/existential-graph/ExistentialGraph.js index 4bc459c..4436769 100644 --- a/client/src/scripts/Paper.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -5,13 +5,29 @@ import Cut from './Cut.js'; import $ from 'jquery'; import _ from 'lodash'; +/** + * @class Existential Graph + * This class is a wrapper around the joint paper, which is the svg canvas that is rendered / the user interacts with. + * The joint paper reflects the graph defined by an associated joint Graph, which is contained in the Sheet class. + */ + +const STATE = { + NO_ACTION: -1, + CREATE: 0, + PROOF_BASE: 1, + INSERT_SUBGRAPH: 2, + ERASE_SUBGRAPH: 3, + INSERT_DBL_CUT: 4, + ERASE_DBL_CUT: 5, +} const PAPER_SIZE = { width: 4000, height: 4000 }; -export default class Paper { + +export default class ExistentialGraph { constructor(dom_id, graph_id) { console.log('LOADING GRAPH', graph_id) this.sheet = new Sheet(this, graph_id); this.dom_element = document.getElementById(dom_id); - this.jpaper = new joint.dia.Paper({ + this.paper = new joint.dia.Paper({ el: this.dom_element, model: this.sheet.graph, width: PAPER_SIZE.width, @@ -20,17 +36,31 @@ export default class Paper { clickThreshold: 1 }); - console.log(getLocalGraphByID(graph_id)) + //default state on creation is NO_ACTION until the graph is initialized + this.state = STATE.NO_ACTION; + + //console.log(getLocalGraphByID(graph_id)) const order = getSafeCellAddOrder(getLocalGraphByID(graph_id).graphJSON.cells); this.addCellsInOrder(order); + // Paper events are callback functions defined on the joint paper that are + // triggered by user input (i.e. keystrokes, clicking, dragging, etc) this.setPaperEvents(); - this.canInsertPremise = true; + //this.canInsertPremise = true; + // TODO: what does this mean? this.previousPremiseCode = -1; + + //the selected premise is the Atomic/Cut that the user is currently interacting / last interacted with this.selected_premise = null; + //The temporary cut is used for: + // The cut seen when creating a cut through dragging. + // When inserting a subgraph with more than one root elements, all elements are placed in a temporary + // cut and inserted to ensure that the level order is preserved, then the temp cut is deleted. this.temp_cut = null; + + this.initial_cut_pos = {x: 0, y: 0}; $(`#${dom_id}`).hover(function() { @@ -40,13 +70,16 @@ export default class Paper { }, function() { this.blur(); }); + + //default state after setup is CREATE mode + this.state = STATE.CREATE; } setPaperEvents(){ // paper events - //arrow functions are required to keep proper context binding - this.jpaper.on("element:mouseenter", ( cellView, evt) =>{ + // arrow functions are required to keep proper context binding + this.paper.on("element:mouseenter", ( cellView, evt ) => { let model = cellView.model let modelView = model.findView(this.jpaper); modelView.showTools() @@ -55,7 +88,7 @@ export default class Paper { this.selected_premise = model }); - this.jpaper.on("element:mouseleave", ( cellView, evt) =>{ + this.paper.on("element:mouseleave", ( cellView, evt ) =>{ let model = cellView.model let modelView = model.findView(this.jpaper); if(!modelView) return; @@ -66,11 +99,8 @@ export default class Paper { }) // First, unembed the cell that has just been grabbed by the user. - this.jpaper.on('cell:pointerdown', (cellView, evt, x, y) => { - - // console.log(cellView) + this.paper.on('cell:pointerdown', (cellView, evt, x, y) => { let cell = cellView.model; - //console.log("cell", cell) if (!cell.get('embeds') || cell.get('embeds').length === 0) { // Show the dragged element above all the other cells (except when the @@ -87,7 +117,7 @@ export default class Paper { // When the dragged cell is dropped over another cell, let it become a child of the // element below. - this.jpaper.on('cell:pointerup', (cellView, evt, x, y) => { + this.paper.on('cell:pointerup', (cellView, evt, x, y) => { let cell = cellView.model; diff --git a/client/src/scripts/Sheet.js b/client/src/existential-graph/Sheet.js similarity index 99% rename from client/src/scripts/Sheet.js rename to client/src/existential-graph/Sheet.js index 83be5ef..6b14aed 100644 --- a/client/src/scripts/Sheet.js +++ b/client/src/existential-graph/Sheet.js @@ -1,8 +1,8 @@ import { getLocalGraphByID, findSmallestCell, color, getCellsBoundingBox, contains, intersects, overlapsCells, cellInArray } from '@util'; import * as joint from 'jointjs' -import Atomic from './Atomic'; -import Cut from './Cut'; +import Atomic from './shapes/Atomic'; +import Cut from './shapes/Cut'; const NSAtomic = joint.dia.Element.define('nameSpace.Atomic',Atomic); const NSCut = joint.dia.Element.define('nameSpace.Cut',Cut); diff --git a/client/src/scripts/Atomic.js b/client/src/existential-graph/shapes/Atomic.js similarity index 100% rename from client/src/scripts/Atomic.js rename to client/src/existential-graph/shapes/Atomic.js diff --git a/client/src/scripts/Cut.js b/client/src/existential-graph/shapes/Cut.js similarity index 100% rename from client/src/scripts/Cut.js rename to client/src/existential-graph/shapes/Cut.js From a548c922f9dc4f4401178875507ecc7f221a1b1b Mon Sep 17 00:00:00 2001 From: Joe Krystowski Date: Sun, 8 Oct 2023 18:13:43 -0400 Subject: [PATCH 02/35] move forceParseCells function --- .../src/existential-graph/ExistentialGraph.js | 122 +----------------- .../{Sheet.js => GraphController.js} | 121 ++++++++++++++++- 2 files changed, 121 insertions(+), 122 deletions(-) rename client/src/existential-graph/{Sheet.js => GraphController.js} (80%) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 4436769..9639f0f 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -1,5 +1,5 @@ import * as joint from 'jointjs'; -import Sheet from './Sheet.js'; +import Sheet from './GraphController.js'; import { getSafeCellAddOrder, getMousePosition, keyCodeIsActive, getMouseIsDown, getLocalGraphByID, contains } from '@util'; import Cut from './Cut.js'; import $ from 'jquery'; @@ -257,126 +257,6 @@ export default class ExistentialGraph { return graphJSON; } - /** - * Force an array of cells into a Cut (target) even if they do not fit by resizing and moving - * the target and its children / neighbors - * @param {Cell[]} cells - * @param {Cut} target - */ - forceParseCells(cells, cellsbbox, target) { - console.clear() - console.log("forcing cells: ",cells) - console.log("to target: ", target) - if (cells === null) return; - if (target === null || target.attributes.type !== "dia.Element.Cut") return; - - // We have a non empty array of cells to insert into a cut - //create a temporary root cut to insert all cells into - const config = { - size: { - width: cellsbbox.width + 10, - height: cellsbbox.height + 10 - }, - position: { - x: cellsbbox.x-10, - y: cellsbbox.y-10 - }, - attrs: { - rect: { - width: cellsbbox.width + 10, - height: cellsbbox.height + 10 - } - } - } - const cut = (new Cut({ - markup: '', - position: { - ...config.position - }, - size: { - ...config.size - }, - attrs: { - rect: { - ...config.attrs.rect - }, - text: { - ...config.attrs.text - }, - level: 0 - }, - // set custom attributes here: - sheet: this.sheet - })).create(config, this.sheet) - // put the cut inside the target - target.embed(cut); - const target_bbox = target.getBoundingBox(); - const cut_bbox = cut.getBoundingBox(); - const buffer = 10; - if (!contains(target_bbox, cut_bbox)) { - //check if premise is to the left of parent - if (cut_bbox.x <= target_bbox.x) { - const diff = target_bbox.x - cut_bbox.x - buffer; - target.position(cut_bbox.x - buffer, target_bbox.y); - target.attr("rect/width", target.attributes.attrs.rect.width + diff); - } - //check if premise is to the right of parent - if (cut_bbox.x + cut_bbox.width >= target_bbox.x + target_bbox.width) { - const diff = cut_bbox.x + cut_bbox.width - (target_bbox.x + target_bbox.width); - target.attr("rect/width", target.attributes.attrs.rect.width + diff + buffer); - } - // check if premise is above parent - if (cut_bbox.y <= target_bbox.y) { - const diff = target_bbox.y - cut_bbox.y - buffer; - target.position(target_bbox.x, cut_bbox.y - buffer); - target.attr("rect/height", target.attributes.attrs.rect.height + diff); - } - //check if premise is below parent - if (cut_bbox.y + cut_bbox.height >= target_bbox.y + target_bbox.height){ - const diff = cut_bbox.y + cut_bbox.height - (target_bbox.y + target_bbox.height) + 10; - target.attr("rect/height", target.attributes.attrs.rect.height + diff + buffer); - } - } - console.log("GHOST CUT: ", cut) - this.sheet.handleCollisions(cut) - - //update position of cells based on where cut ends up - console.log("updating cells",cells); - - for (const cell of cells) { - console.log("updating cell position:",cell.position) - cell.position = { - x: cut.attributes.position.x + (cell.position.x-cellsbbox.x + 5), - y: cut.attributes.position.y + (cell.position.y-cellsbbox.y + 5) - } - } - - const ids = {}; - while (cells.length > 0) { - const cell = cells.shift(); - const type = cell.type; - - if (cell.parent && !ids.hasOwnProperty(cell.parent)) { - //console.log('has parent, skipping for now...') - cells.push(cell); - continue; - } - - if (type === "dia.Element.Cut") { - const new_cut = this.sheet.addCut(cell); - ids[cell.id] = true; - } - else if (type === "dia.Element.Atomic") { - const new_atomic = this.sheet.addAtomic(cell); - ids[cell.id] = true; - } - } - - cut.destroy() - - } - - onKeyDown = (event) => { //backspace (delete premise or cut) if (event.keyCode === 8) { diff --git a/client/src/existential-graph/Sheet.js b/client/src/existential-graph/GraphController.js similarity index 80% rename from client/src/existential-graph/Sheet.js rename to client/src/existential-graph/GraphController.js index 6b14aed..734326a 100644 --- a/client/src/existential-graph/Sheet.js +++ b/client/src/existential-graph/GraphController.js @@ -15,7 +15,7 @@ const DEFAULT_BACKGROUND_COLORS = { } -export default class Sheet { +export default class GraphController { constructor(parent_paper, graph_id) { this.paper = parent_paper; @@ -475,4 +475,123 @@ export default class Sheet { return cell; } + /** + * Force an array of cells into a Cut (target) even if they do not fit by resizing and moving + * the target and its children / neighbors + * @param {Cell[]} cells + * @param {Cut} target + */ + forceParseCells(cells, cellsbbox, target) { + console.clear() + console.log("forcing cells: ",cells) + console.log("to target: ", target) + if (cells === null) return; + if (target === null || target.attributes.type !== "dia.Element.Cut") return; + + // We have a non empty array of cells to insert into a cut + //create a temporary root cut to insert all cells into + const config = { + size: { + width: cellsbbox.width + 10, + height: cellsbbox.height + 10 + }, + position: { + x: cellsbbox.x-10, + y: cellsbbox.y-10 + }, + attrs: { + rect: { + width: cellsbbox.width + 10, + height: cellsbbox.height + 10 + } + } + } + const cut = (new Cut({ + markup: '', + position: { + ...config.position + }, + size: { + ...config.size + }, + attrs: { + rect: { + ...config.attrs.rect + }, + text: { + ...config.attrs.text + }, + level: 0 + }, + // set custom attributes here: + sheet: this + })).create(config, this) + // put the cut inside the target + target.embed(cut); + const target_bbox = target.getBoundingBox(); + const cut_bbox = cut.getBoundingBox(); + const buffer = 10; + if (!contains(target_bbox, cut_bbox)) { + //check if premise is to the left of parent + if (cut_bbox.x <= target_bbox.x) { + const diff = target_bbox.x - cut_bbox.x - buffer; + target.position(cut_bbox.x - buffer, target_bbox.y); + target.attr("rect/width", target.attributes.attrs.rect.width + diff); + } + //check if premise is to the right of parent + if (cut_bbox.x + cut_bbox.width >= target_bbox.x + target_bbox.width) { + const diff = cut_bbox.x + cut_bbox.width - (target_bbox.x + target_bbox.width); + target.attr("rect/width", target.attributes.attrs.rect.width + diff + buffer); + } + // check if premise is above parent + if (cut_bbox.y <= target_bbox.y) { + const diff = target_bbox.y - cut_bbox.y - buffer; + target.position(target_bbox.x, cut_bbox.y - buffer); + target.attr("rect/height", target.attributes.attrs.rect.height + diff); + } + //check if premise is below parent + if (cut_bbox.y + cut_bbox.height >= target_bbox.y + target_bbox.height){ + const diff = cut_bbox.y + cut_bbox.height - (target_bbox.y + target_bbox.height) + 10; + target.attr("rect/height", target.attributes.attrs.rect.height + diff + buffer); + } + } + console.log("GHOST CUT: ", cut) + this.handleCollisions(cut) + + //update position of cells based on where cut ends up + console.log("updating cells",cells); + + for (const cell of cells) { + console.log("updating cell position:",cell.position) + cell.position = { + x: cut.attributes.position.x + (cell.position.x-cellsbbox.x + 5), + y: cut.attributes.position.y + (cell.position.y-cellsbbox.y + 5) + } + } + + const ids = {}; + while (cells.length > 0) { + const cell = cells.shift(); + const type = cell.type; + + if (cell.parent && !ids.hasOwnProperty(cell.parent)) { + //console.log('has parent, skipping for now...') + cells.push(cell); + continue; + } + + if (type === "dia.Element.Cut") { + const new_cut = this.addCut(cell); + ids[cell.id] = true; + } + else if (type === "dia.Element.Atomic") { + const new_atomic = this.addAtomic(cell); + ids[cell.id] = true; + } + } + + cut.destroy() + + } + } \ No newline at end of file From 473f688fb2bc7ea23d108e6fdd24c3b232c483ee Mon Sep 17 00:00:00 2001 From: Joe Krystowski Date: Sun, 8 Oct 2023 22:15:25 -0400 Subject: [PATCH 03/35] Basic stubs for queue and related classes --- client/src/existential-graph/History.js | 23 ++++++++++++++++++ client/src/existential-graph/Item.js | 10 ++++++++ client/src/existential-graph/Proof.js | 16 +++++++++++++ client/src/existential-graph/Queue.js | 32 +++++++++++++++++++++++++ 4 files changed, 81 insertions(+) create mode 100644 client/src/existential-graph/History.js create mode 100644 client/src/existential-graph/Item.js create mode 100644 client/src/existential-graph/Proof.js create mode 100644 client/src/existential-graph/Queue.js diff --git a/client/src/existential-graph/History.js b/client/src/existential-graph/History.js new file mode 100644 index 0000000..856d248 --- /dev/null +++ b/client/src/existential-graph/History.js @@ -0,0 +1,23 @@ +import { Queue } from "./Queue"; + +/** + * A series of phyiscal changes to the graph. + */ + +class History { + constructor() { + this.history = new Queue(); + } + + undo() + { + // TODO + this.history.pop() + } + + do(action) + { + // TODO + this.history.push(action); + } +} \ No newline at end of file diff --git a/client/src/existential-graph/Item.js b/client/src/existential-graph/Item.js new file mode 100644 index 0000000..176e6df --- /dev/null +++ b/client/src/existential-graph/Item.js @@ -0,0 +1,10 @@ + +export default class Item { + constructor(value = null) + { + this.prev = null; + this.next = null; + this.value = value; + } + +} \ No newline at end of file diff --git a/client/src/existential-graph/Proof.js b/client/src/existential-graph/Proof.js new file mode 100644 index 0000000..9d40e20 --- /dev/null +++ b/client/src/existential-graph/Proof.js @@ -0,0 +1,16 @@ +import { Queue } from "./Queue" + +/** + * Proofs are represented as a series of logical steps. This often includes more than one physical change to the graph for a single step + */ +class Proof { + constructor() + { + this.proof = new Queue(); + } + + addStep(step) { + // TODO + this.proof.push(step); + } +} \ No newline at end of file diff --git a/client/src/existential-graph/Queue.js b/client/src/existential-graph/Queue.js new file mode 100644 index 0000000..bef4f9f --- /dev/null +++ b/client/src/existential-graph/Queue.js @@ -0,0 +1,32 @@ +import Item from "./Item"; + +export class Queue +{ + constructor() + { + this.head = new Item("head") + this.tail = new Item("tail"); + this.head.next = this.tail; + this.tail.prev = this.head; + } + + pop() { + let element = this.tail.prev; + this.tail.prev = element.prev; + return this.element.value; + } + + push(val) { + let new_item = new Item(val); + + new_item.prev = this.tail.prev; + new_item.next = this.tail; + + this.tail.prev.next = new_item; + this.tail.prev = new_item; + } + + peek() { + return this.tail.prev.value() + } +} \ No newline at end of file From 1563545fae2777a9326018a1508a4693a72c3a8d Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Sun, 8 Oct 2023 23:17:02 -0400 Subject: [PATCH 04/35] fix compilation errors --- client/src/existential-graph/ExistentialGraph.js | 14 +++++++------- client/src/existential-graph/shapes/Atomic.js | 2 +- client/src/existential-graph/shapes/Cut.js | 2 +- client/src/scripts/CreatePaper.js | 4 ++-- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 9639f0f..7715f3e 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -1,7 +1,7 @@ import * as joint from 'jointjs'; -import Sheet from './GraphController.js'; +import GraphController from './GraphController.js'; import { getSafeCellAddOrder, getMousePosition, keyCodeIsActive, getMouseIsDown, getLocalGraphByID, contains } from '@util'; -import Cut from './Cut.js'; +import Cut from './shapes/Cut.js'; import $ from 'jquery'; import _ from 'lodash'; @@ -25,7 +25,7 @@ const PAPER_SIZE = { width: 4000, height: 4000 }; export default class ExistentialGraph { constructor(dom_id, graph_id) { console.log('LOADING GRAPH', graph_id) - this.sheet = new Sheet(this, graph_id); + this.sheet = new GraphController(this, graph_id); this.dom_element = document.getElementById(dom_id); this.paper = new joint.dia.Paper({ el: this.dom_element, @@ -47,7 +47,7 @@ export default class ExistentialGraph { // triggered by user input (i.e. keystrokes, clicking, dragging, etc) this.setPaperEvents(); - //this.canInsertPremise = true; + this.canInsertPremise = true; // TODO: what does this mean? this.previousPremiseCode = -1; @@ -81,7 +81,7 @@ export default class ExistentialGraph { // arrow functions are required to keep proper context binding this.paper.on("element:mouseenter", ( cellView, evt ) => { let model = cellView.model - let modelView = model.findView(this.jpaper); + let modelView = model.findView(this.paper); modelView.showTools() model.attr("rect/stroke", "red") model.attr("text/fill", "red") @@ -90,7 +90,7 @@ export default class ExistentialGraph { this.paper.on("element:mouseleave", ( cellView, evt ) =>{ let model = cellView.model - let modelView = model.findView(this.jpaper); + let modelView = model.findView(this.paper); if(!modelView) return; modelView.hideTools() model.attr("rect/stroke", "black") @@ -388,7 +388,7 @@ export default class ExistentialGraph { this.sheet.addCut(config); } - this.jpaper.setInteractivity(true); + this.paper.setInteractivity(true); this.temp_cut = null; } diff --git a/client/src/existential-graph/shapes/Atomic.js b/client/src/existential-graph/shapes/Atomic.js index 287b847..e29e398 100644 --- a/client/src/existential-graph/shapes/Atomic.js +++ b/client/src/existential-graph/shapes/Atomic.js @@ -131,7 +131,7 @@ export default class Atomic extends joint.dia.Element { //TODO: see Cut.addTools() addTools(element) { //element view is in charge of rendering the elements on the paper - let elementView = element.findView(element.sheet.paper.jpaper); + let elementView = element.findView(element.sheet.paper.paper); //clear any old tools elementView.removeTools(); // boundary tool shows boundaries of element diff --git a/client/src/existential-graph/shapes/Cut.js b/client/src/existential-graph/shapes/Cut.js index 487beb4..7e52f26 100644 --- a/client/src/existential-graph/shapes/Cut.js +++ b/client/src/existential-graph/shapes/Cut.js @@ -198,7 +198,7 @@ export default class Cut extends joint.dia.Element { /// ( i think we can? ) addTools(element) { //element view is in charge of rendering the elements on the paper - let elementView = element.findView(element.sheet.paper.jpaper); + let elementView = element.findView(element.sheet.paper.paper); //clear any old tools elementView.removeTools(); // boundary tool shows boundaries of element diff --git a/client/src/scripts/CreatePaper.js b/client/src/scripts/CreatePaper.js index 4f6915f..2da84e8 100644 --- a/client/src/scripts/CreatePaper.js +++ b/client/src/scripts/CreatePaper.js @@ -1,8 +1,8 @@ -import Paper from './Paper'; +import Paper from '@root/existential-graph/ExistentialGraph'; export default class CreatePaper extends Paper { constructor(dom_id, graph_id) { super(dom_id, graph_id); - this.jpaper.setInteractivity(true); + this.paper.setInteractivity(true); } } \ No newline at end of file From d5539e639cf653c60c7a9bc37f09eccfd4e11d51 Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Sun, 8 Oct 2023 23:46:15 -0400 Subject: [PATCH 05/35] begin hypergraph implementation --- .../ExistentialHypergraph.js | 36 +++++++++++++++++++ .../ExistentialHypergraphNode.js | 19 ++++++++++ client/src/existential-graph/History.js | 4 +-- .../{Queue.js => LinkedList.js} | 6 ++-- client/src/existential-graph/Proof.js | 16 --------- 5 files changed, 59 insertions(+), 22 deletions(-) create mode 100644 client/src/existential-graph/ExistentialHypergraph.js create mode 100644 client/src/existential-graph/ExistentialHypergraphNode.js rename client/src/existential-graph/{Queue.js => LinkedList.js} (92%) delete mode 100644 client/src/existential-graph/Proof.js diff --git a/client/src/existential-graph/ExistentialHypergraph.js b/client/src/existential-graph/ExistentialHypergraph.js new file mode 100644 index 0000000..56657f6 --- /dev/null +++ b/client/src/existential-graph/ExistentialHypergraph.js @@ -0,0 +1,36 @@ +import { Queue } from "./LinkedList" + +/** + * Existential Hypergraphs are directed graphs in which the nodes represent Existential Graphs and the edges represent applications + * of logical rules to transition from one graph to another. + * + * We represent proofs using Existential Hypergraphs + */ +class ExistentialHypergraph { + constructor(rootGraph) + { + this.root = rootGraph; + } + + addStep(graphId, rule, destination) { + const hypergraphNode = this.find(graphId); + if (hypergraphNode) + hypergraphNode.addTransition(rule, destination); + } + + find(graphId) { + const current = [this.root] + while(current.length > 0) { + let next = [] + for (let graph of current) { + if (graph.id === graphId) + return graph; + next.push(...graph.next); + } + + current = next; + } + + return null; + } +} \ No newline at end of file diff --git a/client/src/existential-graph/ExistentialHypergraphNode.js b/client/src/existential-graph/ExistentialHypergraphNode.js new file mode 100644 index 0000000..99e0f31 --- /dev/null +++ b/client/src/existential-graph/ExistentialHypergraphNode.js @@ -0,0 +1,19 @@ + + +export default class ExistentialHypergraphNode { + constructor(existentialGraph) { + this.value = existentialGraph; + + this.parent = null; + this.next = []; + } + + addTransition(rule, destination) { + this.next.push({ + rule, + destination: new ExistentialHypergraphNode(destination) + }); + } + + +} \ No newline at end of file diff --git a/client/src/existential-graph/History.js b/client/src/existential-graph/History.js index 856d248..8dca939 100644 --- a/client/src/existential-graph/History.js +++ b/client/src/existential-graph/History.js @@ -1,4 +1,4 @@ -import { Queue } from "./Queue"; +import { LinkedList } from "./LinkedList"; /** * A series of phyiscal changes to the graph. @@ -6,7 +6,7 @@ import { Queue } from "./Queue"; class History { constructor() { - this.history = new Queue(); + this.history = new LinkedList(); } undo() diff --git a/client/src/existential-graph/Queue.js b/client/src/existential-graph/LinkedList.js similarity index 92% rename from client/src/existential-graph/Queue.js rename to client/src/existential-graph/LinkedList.js index bef4f9f..9c947d3 100644 --- a/client/src/existential-graph/Queue.js +++ b/client/src/existential-graph/LinkedList.js @@ -1,9 +1,7 @@ import Item from "./Item"; -export class Queue -{ - constructor() - { +export class LinkedList { + constructor() { this.head = new Item("head") this.tail = new Item("tail"); this.head.next = this.tail; diff --git a/client/src/existential-graph/Proof.js b/client/src/existential-graph/Proof.js deleted file mode 100644 index 9d40e20..0000000 --- a/client/src/existential-graph/Proof.js +++ /dev/null @@ -1,16 +0,0 @@ -import { Queue } from "./Queue" - -/** - * Proofs are represented as a series of logical steps. This often includes more than one physical change to the graph for a single step - */ -class Proof { - constructor() - { - this.proof = new Queue(); - } - - addStep(step) { - // TODO - this.proof.push(step); - } -} \ No newline at end of file From 5191415eca7429f02de8878f985de01587a61b4e Mon Sep 17 00:00:00 2001 From: joekrystowski Date: Sat, 21 Oct 2023 20:07:03 -0400 Subject: [PATCH 06/35] add insertion isolation mode to graph controller --- .../src/existential-graph/ExistentialGraph.js | 13 ++- .../src/existential-graph/GraphController.js | 77 +++++++++++++ client/src/existential-graph/shapes/Atomic.js | 109 +++++++++++------- client/src/existential-graph/shapes/Cut.js | 24 +++- 4 files changed, 176 insertions(+), 47 deletions(-) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 7715f3e..e5be05a 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -33,7 +33,16 @@ export default class ExistentialGraph { width: PAPER_SIZE.width, height: PAPER_SIZE.height, preventContextMenu: false, - clickThreshold: 1 + clickThreshold: 1, + interactive: function(cellView) { + if (cellView.model.get("locked")) { + return { + //locking disables moving the element + elementMove: false + } + }; + return true; + } }); //default state on creation is NO_ACTION until the graph is initialized @@ -178,7 +187,7 @@ export default class ExistentialGraph { y: mouse_pos.y - this.dom_element.getBoundingClientRect().top }; } - + /** * diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index 734326a..fbd8a2d 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -594,4 +594,81 @@ export default class GraphController { } + lockAllCells() { + const cells = this.graph.getCells() + + for (let cell of cells) { + cell.lock() + } + } + + unlockAllCells() { + const cells = this.graph.getCells() + + for (let cell of cells) { + cell.unlock() + } + } + + lockSubgraph(root, includeRoot=true) { + if (includeRoot) { + root.lock() + } + + let children = root.getEmbeddedCells(); + while (children.length > 0) { + let new_children = [] + for (let child of children) { + new_children.push(...child.getEmbeddedCells()); + child.lock(); + } + children = new_children + } + } + + unlockSubgraph(root) { + root.unlock() + let children = root.getEmbeddedCells(); + while (children.length > 0) { + let new_children = [] + for (let child of children) { + new_children.push(...child.getEmbeddedCells()); + child.unlock(); + } + children = new_children + } + } + + //insertion mode disables editing all elements except for those on the same level with the target cut + enableInsertMode(targetCut) { + const type = targetCut.type + + if (type == "dia.Element.Premise") { + //error : can not activate insert mode on a premise + return null; + } + + //start by locking all cells + this.lockAllCells() + + //remove joint tools from cells + + + //unlock children of target cut + const children = targetCut.getEmbeddedCells() + for (const child of children) { + child.unlock() + } + } + + //insertion mode disables editing all elements except for those on the same level with the target cut + disableInsertMode() { + //unlock all cells + const cells = this.graph.getCells(); + + for (const cell of cells) { + cell.unlock() + } + } + } \ No newline at end of file diff --git a/client/src/existential-graph/shapes/Atomic.js b/client/src/existential-graph/shapes/Atomic.js index e29e398..8da4ef8 100644 --- a/client/src/existential-graph/shapes/Atomic.js +++ b/client/src/existential-graph/shapes/Atomic.js @@ -40,7 +40,8 @@ export default class Atomic extends joint.dia.Element { type: "dia.Element.Atomic", attrs: { rect: ATOMIC_DEFAULTS.attrs.rect, - text: ATOMIC_DEFAULTS.attrs.text + text: ATOMIC_DEFAULTS.attrs.text, + locked: false } } } @@ -103,54 +104,74 @@ export default class Atomic extends joint.dia.Element { //this.sheet.paper.handleDeleteCell(); } - obliterate() { - this.destroy(); - } - - active() { - return; - } - - inactive(){ - return; - } - - getBoundingBox() { - return { - width: this.attributes.attrs.rect.width, - height: this.attributes.attrs.rect.height, - x: this.attributes.position.x, - y: this.attributes.position.y - } - } - - getArea() { - return this.attributes.attrs.rect.width * this.attributes.attrs.rect.height; - } + obliterate() { + this.destroy(); + } - //TODO: see Cut.addTools() - addTools(element) { - //element view is in charge of rendering the elements on the paper + active() { + return; + } + + inactive(){ + return; + } + + getBoundingBox() { + return { + width: this.attributes.attrs.rect.width, + height: this.attributes.attrs.rect.height, + x: this.attributes.position.x, + y: this.attributes.position.y + } + } + + getArea() { + return this.attributes.attrs.rect.width * this.attributes.attrs.rect.height; + } + + enableTools() { let elementView = element.findView(element.sheet.paper.paper); - //clear any old tools - elementView.removeTools(); - // boundary tool shows boundaries of element - let boundaryTool = new joint.elementTools.Boundary(); - - let rect_tools = [boundaryTool]; - - let toolsView = new joint.dia.ToolsView({ - tools: rect_tools - }); + elementView.showTools(); + } - elementView.addTools(toolsView); - //start with tools hidden + disableTools() { + let elementView = element.findView(element.sheet.paper.paper); elementView.hideTools(); - // element.on("change:position", function (eventView) { - // element.toFront(); - // }); - // --- end of paper events ----- } + + lock() { + this.set('locked', true) + this.disableTools() + } + + unlock () { + this.set('locked', false) + this.enableTools() + } + + //TODO: see Cut.addTools() + addTools(element) { + //element view is in charge of rendering the elements on the paper + let elementView = element.findView(element.sheet.paper.paper); + //clear any old tools + elementView.removeTools(); + // boundary tool shows boundaries of element + let boundaryTool = new joint.elementTools.Boundary(); + + let rect_tools = [boundaryTool]; + + let toolsView = new joint.dia.ToolsView({ + tools: rect_tools + }); + + elementView.addTools(toolsView); + //start with tools hidden + elementView.hideTools(); + // element.on("change:position", function (eventView) { + // element.toFront(); + // }); + // --- end of paper events ----- + } } diff --git a/client/src/existential-graph/shapes/Cut.js b/client/src/existential-graph/shapes/Cut.js index 7e52f26..dcd0a40 100644 --- a/client/src/existential-graph/shapes/Cut.js +++ b/client/src/existential-graph/shapes/Cut.js @@ -43,7 +43,8 @@ export default class Cut extends joint.dia.Element { type: "dia.Element.Cut", attrs: { rect: CUT_DEFAULTS.attrs.rect, - text: CUT_DEFAULTS.attrs.text + text: CUT_DEFAULTS.attrs.text, + locked: false } } } @@ -245,6 +246,27 @@ export default class Cut extends joint.dia.Element { // }); // --- end of paper events ----- } + + enableTools() { + let elementView = element.findView(element.sheet.paper.paper); + elementView.showTools(); + } + + disableTools() { + let elementView = element.findView(element.sheet.paper.paper); + elementView.hideTools(); + } + + lock() { + this.set('locked', true) + this.disableTools() + } + + unlock () { + this.set('locked', false) + this.enableTools() + } + } From 94cf370742f83c326038a1a10e7738b035f01e0d Mon Sep 17 00:00:00 2001 From: joekrystowski Date: Sat, 21 Oct 2023 20:16:02 -0400 Subject: [PATCH 07/35] insertDoubleCut for graphController --- .../src/existential-graph/GraphController.js | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index fbd8a2d..3608276 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -671,4 +671,50 @@ export default class GraphController { } } + addCutAsParent(child) { + const cut = (new Cut()).create(config, this, false); + + } + + insertDoubleCut = function(sheet, model, mousePosition={}) { + let position = {}; + let size = {} + if (!model && mousePosition) { + position = mousePosition; + size = { width: 80, height: 80 } + } + else if (model){ + position = model.get('position'); + size = { width: model.attr('rect/width'), height: model.attr('rect/height') } + } + else { + throw new Error('Bad arguments'); + } + const multipliers = [0.8, 0.25]; + let new_cuts = [] + for(let i = 0; i < multipliers.length; i++) { + new_cuts.push(sheet.addCut({ + position: { + x: position.x - (size.width * multipliers[i]/2), + y: position.y - (size.height * multipliers[i]/2) + }, + attrs: { + rect: { + width: size.width * (1 + multipliers[i]), + height: size.height * (1 + multipliers[i]) + } + } + }, false)); + } + new_cuts[0].embed(new_cuts[1]) + this.colorByLevel(new_cuts[0]) + let selected_premise = this.paper.selected_premise; + if (selected_premise && selected_premise.attributes.type === "dia.Element.Cut") { + selected_premise.embed(new_cuts[0]); + this.colorByLevel(selected_premise) + this.pack(selected_premise) + } + this.handleCollisions(new_cuts[0]) + } + } \ No newline at end of file From bd5f1b7ad08d9010ce8ccfe3d0a7beafa5b21df9 Mon Sep 17 00:00:00 2001 From: joekrystowski Date: Sat, 21 Oct 2023 22:52:57 -0400 Subject: [PATCH 08/35] delete double cut for graph controller --- .../src/existential-graph/GraphController.js | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index 3608276..e92ded3 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -717,4 +717,25 @@ export default class GraphController { this.handleCollisions(new_cuts[0]) } + deleteDoubleCut = function(sheet, model) { + console.log("MODEL: ", model); + const graph = sheet.graph; + if(model.__proto__.constructor.name === "Cut" && model.attributes.embeds?.length === 1 && + graph.getCell(model.attributes.embeds[0]).__proto__.constructor.name === "Cut") { + const children = graph.getCell(model.attributes.embeds[0]).attributes.embeds; + graph.getCell(model.attributes.embeds[0]).destroy(); + model.destroy(); + if(model.attributes.parent) { + sheet.handleCollisions(graph.getCell(model.attributes.parent)); + } + else { + children?.forEach(element => { + if(graph.getCell(element).__proto__.constructor.name === "Cut") { + sheet.handleCollisions(graph.getCell(element)) + } + }); + } + } + } + } \ No newline at end of file From 51f384c4de1b0af133e441ee0880afc0d5a26553 Mon Sep 17 00:00:00 2001 From: joekrystowski Date: Sat, 21 Oct 2023 22:59:09 -0400 Subject: [PATCH 09/35] delete subgraph function --- client/src/existential-graph/GraphController.js | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index e92ded3..acda863 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -738,4 +738,14 @@ export default class GraphController { } } + deleteSubgraph(root, deleteRoot=true) { + //destroy recursively, starting at the leaves to not lose reference + //to the rest of the tree by deleting the root first + let children = root.getEmbeddedCells() + for (const child in children) { + this.deleteSubgraph(child) + } + root.destroy() + } + } \ No newline at end of file From f4fa5ca51b874199a6826509ee7e352c41492f29 Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Sat, 21 Oct 2023 23:20:46 -0400 Subject: [PATCH 10/35] Add functionality to new toolbar buttons with graph controller --- .../Toolbar/GraphTool/GraphTool.jsx | 11 +++ client/src/components/Toolbar/Toolbar.jsx | 33 ++----- .../src/existential-graph/ExistentialGraph.js | 98 +++++++++++-------- client/src/main.css | 20 ++-- client/src/views/Create/Create.jsx | 18 ++-- client/src/views/Dashboard/Dashboard.css | 8 ++ 6 files changed, 105 insertions(+), 83 deletions(-) create mode 100644 client/src/components/Toolbar/GraphTool/GraphTool.jsx diff --git a/client/src/components/Toolbar/GraphTool/GraphTool.jsx b/client/src/components/Toolbar/GraphTool/GraphTool.jsx new file mode 100644 index 0000000..bb694c1 --- /dev/null +++ b/client/src/components/Toolbar/GraphTool/GraphTool.jsx @@ -0,0 +1,11 @@ +import React from 'react'; + +export default function GraphTool(props) { + return ( +
+ + {props.children} +
+ ); +} \ No newline at end of file diff --git a/client/src/components/Toolbar/Toolbar.jsx b/client/src/components/Toolbar/Toolbar.jsx index 4ad95b9..8fb5f55 100644 --- a/client/src/components/Toolbar/Toolbar.jsx +++ b/client/src/components/Toolbar/Toolbar.jsx @@ -3,11 +3,10 @@ import "@root/main.css"; // Tawilwind stylesheet import ToolbarItem from './ToolbarItem/ToolbarItem'; import ToolbarItemOption from './ToolbarItemOption/ToolbarItemOption'; import { Menu } from '@headlessui/react'; +import GraphTool from './GraphTool/GraphTool'; export default function Toolbar( props ) { - - function handleGraphNameLoseFocus(e) { e.target.value = e.target.value.trim(); if (!e.target.value) e.target.value = "Untitled Graph"; @@ -52,31 +51,11 @@ export default function Toolbar( props ) { {/* Graph tools */}
-
- - Cut -
-
- - Insert Double Cut -
-
- - Erase Double Cut -
-
- - Insert Subgraph -
-
- - Erase Subgraph -
+ props.handleSetGraphTool('cut')}>Cut + props.handleSetGraphTool('insert_double_cut')}>Insert Double Cut + props.handleSetGraphTool('erase_double_cut')}>Erase Double Cut + props.handleSetGraphTool('insert_subgraph')}>Insert Subgraph + props.handleSetGraphTool('erase_subgraph')}>Erase Subgraph
); diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 7715f3e..cbd54af 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -60,6 +60,9 @@ export default class ExistentialGraph { // cut and inserted to ensure that the level order is preserved, then the temp cut is deleted. this.temp_cut = null; + // Name of action selected by toolbar graph tool buttons + this.graphTool = null; + this.initial_cut_pos = {x: 0, y: 0}; @@ -137,33 +140,6 @@ export default class ExistentialGraph { // this.sheet.graph.on('add', () => { // this.onGraphUpdate(); // }); - - //PAPER UNDO AND REDO EVENTS - if (false) { - // $(this.dom_element).on('keydown', (event) => { - // if (event.keyCode === 90 && (event.ctrlKey || event.metaKey) && !event.shiftKey) { - // const new_state = this.history.current.undo(); - // this.selected_premise = null; - // //only update graph if new state exists - // //undo will return false if can't undo anymore - // if (new_state) { - // this.history.current.lock(); - // this.sheet.importCells(new_state); - // this.history.current.unlock(); - // } - // } - // if (event.keyCode === 90 && (event.ctrlKey || event.metaKey) && event.shiftKey) { - // const new_state = this.history.current.redo(); - // //only update graph if new state exists - // //redo will return false if can't redo anymore - // if (new_state) { - // this.history.current.lock(); - // this.sheet.importCells(new_state); - // this.history.current.unlock(); - // } - // } - // }); - } } @@ -336,6 +312,9 @@ export default class ExistentialGraph { } onMouseDown = (event) => { + + if (this.graphTool) return; + //console.log('mousedown', this); if (keyCodeIsActive(16) /*&& this.getMode() === 'create'*/) { this.initial_cut_pos = this.getRelativeMousePos(); @@ -353,21 +332,62 @@ export default class ExistentialGraph { } onMouseUp = () => { - //console.log('mouseup', this); - if (false/*this.getMode() === 'proof'*/) { - //this.history.current.startBatch(); - if (!this.selected_premise && this.props.action && this.props.action.name === 'insertDoubleCut') { - const mouse_adjusted = this.getRelativeMousePos(); - this.props.action(this.sheet, null, mouse_adjusted); - this.props.handleClearAction(); + + if (this.graphTool) { + console.log('executing ', this.graphTool); + + if (this.graphTool === 'cut') { + let config = { + position: this.getRelativeMousePos() + } + if (this.selected_premise) { + config["child"] = this.selected_premise; + this.sheet.addCut(config); + } else { + this.sheet.addCut(config); + } } - if (!this.selected_premise && this.props.action && this.props.action.name === 'bound iterationend') { - const mouse_adjusted = this.getRelativeMousePos(); - this.props.action(this.sheet, null, mouse_adjusted); - this.props.handleClearAction(); + else if (this.graphTool === 'insert_double_cut') { + let config = { + position: this.getRelativeMousePos() + } + + let cut1; + if (this.selected_premise) { + config["child"] = this.selected_premise; + cut1 = this.sheet.addCut(config); + } else { + cut1 = this.sheet.addCut(config); + } + + config["child"] = cut1; + this.sheet.addCut(config); + } - //this.history.current.endBatch(); + else if (this.graphTool === 'erase_double_cut') { + let config = { + position: this.getRelativeMousePos() + } + this.sheet.erase_double_cut(config); + } + else if (this.graphTool === 'insert_subgraph') { + let config = { + position: this.getRelativeMousePos() + } + this.sheet.insert_subgraph(config); + } + else if (this.graphTool === 'erase_subgraph') { + let config = { + position: this.getRelativeMousePos() + } + this.sheet.erase_subgraph(config); + } + + + this.graphTool = null; + return } + if (this.temp_cut /*&& this.getMode() === 'create'*/) { const position = _.clone(this.temp_cut.get('position')); const size = _.clone({width: this.temp_cut.attr('rect/width'), height: this.temp_cut.attr('rect/height')}); diff --git a/client/src/main.css b/client/src/main.css index 1b36280..f6f7b20 100644 --- a/client/src/main.css +++ b/client/src/main.css @@ -622,11 +622,6 @@ video { height: max-content; } -.h-min { - height: -webkit-min-content; - height: min-content; -} - .h-10 { height: 2.5rem; } @@ -635,6 +630,11 @@ video { height: 83.333333%; } +.h-min { + height: -webkit-min-content; + height: min-content; +} + .min-h-\[2rem\] { min-height: 2rem; } @@ -807,11 +807,6 @@ video { background-color: transparent; } -.bg-slate-600 { - --tw-bg-opacity: 1; - background-color: rgb(71 85 105 / var(--tw-bg-opacity)); -} - .bg-blue-500 { --tw-bg-opacity: 1; background-color: rgb(59 130 246 / var(--tw-bg-opacity)); @@ -827,6 +822,11 @@ video { background-color: rgb(148 163 184 / var(--tw-bg-opacity)); } +.bg-slate-600 { + --tw-bg-opacity: 1; + background-color: rgb(71 85 105 / var(--tw-bg-opacity)); +} + .p-5 { padding: 1.25rem; } diff --git a/client/src/views/Create/Create.jsx b/client/src/views/Create/Create.jsx index 7bd7c71..6bacea1 100644 --- a/client/src/views/Create/Create.jsx +++ b/client/src/views/Create/Create.jsx @@ -3,9 +3,8 @@ import { useState, useRef, useEffect } from 'react'; import { useParams } from 'react-router-dom'; import Toolbar from '@components/Toolbar/Toolbar.jsx'; import { CreatePaperComponent } from '@components/Paper'; -import CreatePaper from '@scripts/CreatePaper'; +import ExistentialGraph from '../../existential-graph/ExistentialGraph'; -import { create } from 'lodash'; import { addToLocalGraphData, getLocalGraphByID } from '../../util/util'; export default function Create(props) { @@ -13,17 +12,16 @@ export default function Create(props) { const { id } = useParams(); console.log('default name', getLocalGraphByID(id).name); const [graphName, setGraphName] = useState(getLocalGraphByID(id).name); - const [paper, setPaper] = useState(null); - + const [eg, setExistentialGraph] = useState(null); useEffect(() => { - setPaper(new CreatePaper('main-paper', id)); + setExistentialGraph(new ExistentialGraph('main-paper', id)); }, [id]); const handleSaveGraph = () => { console.log('CREATE VIEW SAVING GRAPH', graphName, id); - const graphJSON = paper.exportGraphAsJSON(); + const graphJSON = eg.exportGraphAsJSON(); console.log(graphJSON) addToLocalGraphData(id, graphJSON, graphName) } @@ -32,6 +30,11 @@ export default function Create(props) { setGraphName(newName); } + const handleSetGraphTool = (graphTool) => { + console.log('set graph tool:', graphTool); + eg.graphTool = graphTool; + } + return (
@@ -40,9 +43,10 @@ export default function Create(props) { graphName={graphName} handleGraphNameUpdate={handleGraphNameUpdate} handleSaveGraph={handleSaveGraph} + handleSetGraphTool={handleSetGraphTool} /> diff --git a/client/src/views/Dashboard/Dashboard.css b/client/src/views/Dashboard/Dashboard.css index b500c45..c0630e9 100644 --- a/client/src/views/Dashboard/Dashboard.css +++ b/client/src/views/Dashboard/Dashboard.css @@ -77,6 +77,14 @@ color: black; } +.graph-table-item:nth-child(even) { + background-color: #ffffff; +} + +.graph-table-item:nth-child(odd) { + background-color: #e8f1ff; +} + .graph-table-item:hover { cursor: pointer; background-color: #8792a5; From 6322b6c04c23784edbfe9db969522e1369a6bd30 Mon Sep 17 00:00:00 2001 From: Joe Krystowski Date: Fri, 27 Oct 2023 21:15:41 -0400 Subject: [PATCH 11/35] toggle disabled colors for insertion mode --- .../src/existential-graph/GraphController.js | 26 ++++++++++++++++++- client/src/existential-graph/shapes/Atomic.js | 4 +++ client/src/existential-graph/shapes/Cut.js | 4 +++ client/src/util/color-util.js | 15 +++++++++++ 4 files changed, 48 insertions(+), 1 deletion(-) diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index acda863..3efb3ae 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -14,6 +14,11 @@ const DEFAULT_BACKGROUND_COLORS = { atomic: color.shapes.background.default.color } +const DISABLED_BACKGROUND_COLORS = { + even: color.shapes.disabled.even.inactive, + odd: color.shapes.disabled.odd.inactive, + atomic: color.shapes.disabled.default.color +} export default class GraphController { constructor(parent_paper, graph_id) { @@ -639,6 +644,20 @@ export default class GraphController { } } + colorCells(color_config, cells=[]) { + // if no cells are provided, color all cells + if (cells.length === 0) { + cells = this.graph.getCells() + } + + for (let i = 0; i < cells.length; i++) { + const cell = cells[i] + const level = cell.attributes.attrs.level + const color = (level % 2 === 0) ? color_config.even.color : color_config.odd.color + cell.setColor(color) + } + } + //insertion mode disables editing all elements except for those on the same level with the target cut enableInsertMode(targetCut) { const type = targetCut.type @@ -652,13 +671,18 @@ export default class GraphController { this.lockAllCells() //remove joint tools from cells - + + //color all cells with disabled colors + this.colorCells(DISABLED_BACKGROUND_COLORS) //unlock children of target cut const children = targetCut.getEmbeddedCells() for (const child of children) { child.unlock() } + + //set color to active for target and children + this.colorCells(DEFAULT_BACKGROUND_COLORS, [target, ...children]) } //insertion mode disables editing all elements except for those on the same level with the target cut diff --git a/client/src/existential-graph/shapes/Atomic.js b/client/src/existential-graph/shapes/Atomic.js index 8da4ef8..873583a 100644 --- a/client/src/existential-graph/shapes/Atomic.js +++ b/client/src/existential-graph/shapes/Atomic.js @@ -148,6 +148,10 @@ export default class Atomic extends joint.dia.Element { this.set('locked', false) this.enableTools() } + + setColor(color) { + this.attr("rect/fill", color) + } //TODO: see Cut.addTools() addTools(element) { diff --git a/client/src/existential-graph/shapes/Cut.js b/client/src/existential-graph/shapes/Cut.js index dcd0a40..3ff5b11 100644 --- a/client/src/existential-graph/shapes/Cut.js +++ b/client/src/existential-graph/shapes/Cut.js @@ -175,6 +175,10 @@ export default class Cut extends joint.dia.Element { return this.attributes.attrs.rect.width * this.attributes.attrs.rect.height; } + setColor(color) { + this.attr("rect/fill", color) + } + // move(position, timestep = 1000, frames = 500) { // let difference = { // x: position.x - this.attributes.position.x, diff --git a/client/src/util/color-util.js b/client/src/util/color-util.js index 23d1536..ffc5f26 100644 --- a/client/src/util/color-util.js +++ b/client/src/util/color-util.js @@ -13,5 +13,20 @@ export let color = { color: "#ffffff00" } } + }, + disabled: { + background: { + odd: { + inactive: "#f2f8fc", + active: "#f2f8fcE0" + }, + even: { + inactive: "#ffffff", + active: "#ffffffE0" + }, + default: { + color: "#ffffff00" + } + } } } \ No newline at end of file From 432c438773f5908cebfc15ad7ed77275c12af02c Mon Sep 17 00:00:00 2001 From: Joe Krystowski Date: Fri, 27 Oct 2023 21:17:01 -0400 Subject: [PATCH 12/35] return color to defaults after insertion --- client/src/existential-graph/GraphController.js | 3 +++ 1 file changed, 3 insertions(+) diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index 3efb3ae..eda9f66 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -693,6 +693,9 @@ export default class GraphController { for (const cell of cells) { cell.unlock() } + + //color all cells with default colors + this.colorCells(DEFAULT_BACKGROUND_COLORS) } addCutAsParent(child) { From 08c8e70578eaa5981dd06effa18dcbd7830e7ddd Mon Sep 17 00:00:00 2001 From: Joe Krystowski Date: Fri, 27 Oct 2023 21:25:58 -0400 Subject: [PATCH 13/35] remove unecessary variables from deleteDoubleCut method --- client/src/existential-graph/GraphController.js | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index eda9f66..0e6025a 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -744,21 +744,20 @@ export default class GraphController { this.handleCollisions(new_cuts[0]) } - deleteDoubleCut = function(sheet, model) { + deleteDoubleCut = function(model) { console.log("MODEL: ", model); - const graph = sheet.graph; if(model.__proto__.constructor.name === "Cut" && model.attributes.embeds?.length === 1 && - graph.getCell(model.attributes.embeds[0]).__proto__.constructor.name === "Cut") { - const children = graph.getCell(model.attributes.embeds[0]).attributes.embeds; - graph.getCell(model.attributes.embeds[0]).destroy(); + this.graph.getCell(model.attributes.embeds[0]).__proto__.constructor.name === "Cut") { + const children = this.graph.getCell(model.attributes.embeds[0]).attributes.embeds; + this.graph.getCell(model.attributes.embeds[0]).destroy(); model.destroy(); if(model.attributes.parent) { - sheet.handleCollisions(graph.getCell(model.attributes.parent)); + this.handleCollisions(this.graph.getCell(model.attributes.parent)); } else { children?.forEach(element => { - if(graph.getCell(element).__proto__.constructor.name === "Cut") { - sheet.handleCollisions(graph.getCell(element)) + if(this.graph.getCell(element).__proto__.constructor.name === "Cut") { + this.handleCollisions(this.graph.getCell(element)) } }); } From de2c5a5cfe36a62cd83ef764c4be3e879eabe87b Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Fri, 27 Oct 2023 21:49:42 -0400 Subject: [PATCH 14/35] integrate with graphcontroller and fix compilation errors --- .../src/existential-graph/ExistentialGraph.js | 51 +++++-------------- .../src/existential-graph/GraphController.js | 24 ++++----- client/src/existential-graph/shapes/Atomic.js | 8 +-- client/src/existential-graph/shapes/Cut.js | 4 +- 4 files changed, 29 insertions(+), 58 deletions(-) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index dc293c8..f26ff67 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -357,39 +357,16 @@ export default class ExistentialGraph { } } else if (this.graphTool === 'insert_double_cut') { - let config = { - position: this.getRelativeMousePos() - } - - let cut1; - if (this.selected_premise) { - config["child"] = this.selected_premise; - cut1 = this.sheet.addCut(config); - } else { - cut1 = this.sheet.addCut(config); - } - - config["child"] = cut1; - this.sheet.addCut(config); - + this.sheet.insertDoubleCut(this.selected_premise, this.getRelativeMousePos()) } else if (this.graphTool === 'erase_double_cut') { - let config = { - position: this.getRelativeMousePos() - } - this.sheet.erase_double_cut(config); + this.sheet.deleteDoubleCut(this.selected_premise); } else if (this.graphTool === 'insert_subgraph') { - let config = { - position: this.getRelativeMousePos() - } - this.sheet.insert_subgraph(config); + this.sheet.enableInsertMode(this.selected_premise); } else if (this.graphTool === 'erase_subgraph') { - let config = { - position: this.getRelativeMousePos() - } - this.sheet.erase_subgraph(config); + this.sheet.deleteSubgraph(this.selected_premise); } @@ -422,18 +399,14 @@ export default class ExistentialGraph { } onMouseMove = () => { - //console.log('mousemove', this); - if(true/*this.getMode() === 'create'*/){ - //console.log(E.isMouseDown); - if (getMouseIsDown() && keyCodeIsActive(16) && this.temp_cut) { - const mouse_adjusted = this.getRelativeMousePos(); - this.temp_cut.set('position', { - x: Math.min(mouse_adjusted.x, this.initial_cut_pos.x), - y: Math.min(mouse_adjusted.y, this.initial_cut_pos.y) - }); - this.temp_cut.attr('rect/width', Math.abs(mouse_adjusted.x - this.initial_cut_pos.x)); - this.temp_cut.attr('rect/height', Math.abs(mouse_adjusted.y - this.initial_cut_pos.y)); - } + if (getMouseIsDown() && keyCodeIsActive(16) && this.temp_cut) { + const mouse_adjusted = this.getRelativeMousePos(); + this.temp_cut.set('position', { + x: Math.min(mouse_adjusted.x, this.initial_cut_pos.x), + y: Math.min(mouse_adjusted.y, this.initial_cut_pos.y) + }); + this.temp_cut.attr('rect/width', Math.abs(mouse_adjusted.x - this.initial_cut_pos.x)); + this.temp_cut.attr('rect/height', Math.abs(mouse_adjusted.y - this.initial_cut_pos.y)); } } } \ No newline at end of file diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index eda9f66..6bd93e1 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -682,7 +682,7 @@ export default class GraphController { } //set color to active for target and children - this.colorCells(DEFAULT_BACKGROUND_COLORS, [target, ...children]) + this.colorCells(DEFAULT_BACKGROUND_COLORS, [targetCut, ...children]) } //insertion mode disables editing all elements except for those on the same level with the target cut @@ -698,12 +698,11 @@ export default class GraphController { this.colorCells(DEFAULT_BACKGROUND_COLORS) } - addCutAsParent(child) { + addCutAsParent(config) { const cut = (new Cut()).create(config, this, false); - } - insertDoubleCut = function(sheet, model, mousePosition={}) { + insertDoubleCut = function(model, mousePosition={}) { let position = {}; let size = {} if (!model && mousePosition) { @@ -720,7 +719,7 @@ export default class GraphController { const multipliers = [0.8, 0.25]; let new_cuts = [] for(let i = 0; i < multipliers.length; i++) { - new_cuts.push(sheet.addCut({ + new_cuts.push(this.addCut({ position: { x: position.x - (size.width * multipliers[i]/2), y: position.y - (size.height * multipliers[i]/2) @@ -744,21 +743,20 @@ export default class GraphController { this.handleCollisions(new_cuts[0]) } - deleteDoubleCut = function(sheet, model) { + deleteDoubleCut(model) { console.log("MODEL: ", model); - const graph = sheet.graph; if(model.__proto__.constructor.name === "Cut" && model.attributes.embeds?.length === 1 && - graph.getCell(model.attributes.embeds[0]).__proto__.constructor.name === "Cut") { - const children = graph.getCell(model.attributes.embeds[0]).attributes.embeds; - graph.getCell(model.attributes.embeds[0]).destroy(); + this.graph.getCell(model.attributes.embeds[0]).__proto__.constructor.name === "Cut") { + const children = this.graph.getCell(model.attributes.embeds[0]).attributes.embeds; + this.graph.getCell(model.attributes.embeds[0]).destroy(); model.destroy(); if(model.attributes.parent) { - sheet.handleCollisions(graph.getCell(model.attributes.parent)); + this.handleCollisions(this.graph.getCell(model.attributes.parent)); } else { children?.forEach(element => { - if(graph.getCell(element).__proto__.constructor.name === "Cut") { - sheet.handleCollisions(graph.getCell(element)) + if(this.graph.getCell(element).__proto__.constructor.name === "Cut") { + this.handleCollisions(this.graph.getCell(element)) } }); } diff --git a/client/src/existential-graph/shapes/Atomic.js b/client/src/existential-graph/shapes/Atomic.js index 873583a..d370307 100644 --- a/client/src/existential-graph/shapes/Atomic.js +++ b/client/src/existential-graph/shapes/Atomic.js @@ -130,13 +130,13 @@ export default class Atomic extends joint.dia.Element { } enableTools() { - let elementView = element.findView(element.sheet.paper.paper); - elementView.showTools(); + let elementView = this.findView(this.sheet.paper.paper); + this.showTools(); } disableTools() { - let elementView = element.findView(element.sheet.paper.paper); - elementView.hideTools(); + let elementView = this.findView(this.sheet.paper.paper); + this.hideTools(); } lock() { diff --git a/client/src/existential-graph/shapes/Cut.js b/client/src/existential-graph/shapes/Cut.js index 3ff5b11..3fd7b49 100644 --- a/client/src/existential-graph/shapes/Cut.js +++ b/client/src/existential-graph/shapes/Cut.js @@ -252,12 +252,12 @@ export default class Cut extends joint.dia.Element { } enableTools() { - let elementView = element.findView(element.sheet.paper.paper); + let elementView = this.findView(this.sheet.paper.paper); elementView.showTools(); } disableTools() { - let elementView = element.findView(element.sheet.paper.paper); + let elementView = this.findView(this.sheet.paper.paper); elementView.hideTools(); } From 05e2b2c2efe735b7b13038074a058c3e4d69d715 Mon Sep 17 00:00:00 2001 From: Joe Krystowski Date: Fri, 27 Oct 2023 21:55:35 -0400 Subject: [PATCH 15/35] fix color config compilation issues --- client/src/util/color-util.js | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/client/src/util/color-util.js b/client/src/util/color-util.js index ffc5f26..34115f2 100644 --- a/client/src/util/color-util.js +++ b/client/src/util/color-util.js @@ -12,10 +12,8 @@ export let color = { default: { color: "#ffffff00" } - } - }, - disabled: { - background: { + }, + disabled: { odd: { inactive: "#f2f8fc", active: "#f2f8fcE0" From 213359bb4e91439267a5b16faeb102b10333c3e0 Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Fri, 27 Oct 2023 22:18:47 -0400 Subject: [PATCH 16/35] add ui indicator for selected graph tool --- .../Toolbar/GraphTool/GraphTool.jsx | 3 +- client/src/components/Toolbar/Toolbar.jsx | 35 ++++++++++++++++--- .../src/existential-graph/GraphController.js | 8 ----- client/src/main.css | 10 ++++++ client/src/views/Create/Create.jsx | 3 ++ 5 files changed, 45 insertions(+), 14 deletions(-) diff --git a/client/src/components/Toolbar/GraphTool/GraphTool.jsx b/client/src/components/Toolbar/GraphTool/GraphTool.jsx index bb694c1..20b9125 100644 --- a/client/src/components/Toolbar/GraphTool/GraphTool.jsx +++ b/client/src/components/Toolbar/GraphTool/GraphTool.jsx @@ -1,11 +1,12 @@ import React from 'react'; export default function GraphTool(props) { + return (
- {props.children} + {props.children}
); } \ No newline at end of file diff --git a/client/src/components/Toolbar/Toolbar.jsx b/client/src/components/Toolbar/Toolbar.jsx index 8fb5f55..b3709db 100644 --- a/client/src/components/Toolbar/Toolbar.jsx +++ b/client/src/components/Toolbar/Toolbar.jsx @@ -51,11 +51,36 @@ export default function Toolbar( props ) { {/* Graph tools */}
- props.handleSetGraphTool('cut')}>Cut - props.handleSetGraphTool('insert_double_cut')}>Insert Double Cut - props.handleSetGraphTool('erase_double_cut')}>Erase Double Cut - props.handleSetGraphTool('insert_subgraph')}>Insert Subgraph - props.handleSetGraphTool('erase_subgraph')}>Erase Subgraph + props.handleSetGraphTool('cut')} + > + Cut + + props.handleSetGraphTool('insert_double_cut')} + > + Insert Double Cut + + props.handleSetGraphTool('erase_double_cut')} + > + Erase Double Cut + + props.handleSetGraphTool('insert_subgraph')} + > + Insert Subgraph + + props.handleSetGraphTool('erase_subgraph')} + > + Erase Subgraph +
); diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index 03f1fe8..6bd93e1 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -743,11 +743,7 @@ export default class GraphController { this.handleCollisions(new_cuts[0]) } -<<<<<<< HEAD deleteDoubleCut(model) { -======= - deleteDoubleCut = function(model) { ->>>>>>> 08c8e70578eaa5981dd06effa18dcbd7830e7ddd console.log("MODEL: ", model); if(model.__proto__.constructor.name === "Cut" && model.attributes.embeds?.length === 1 && this.graph.getCell(model.attributes.embeds[0]).__proto__.constructor.name === "Cut") { @@ -755,11 +751,7 @@ export default class GraphController { this.graph.getCell(model.attributes.embeds[0]).destroy(); model.destroy(); if(model.attributes.parent) { -<<<<<<< HEAD this.handleCollisions(this.graph.getCell(model.attributes.parent)); -======= - this.handleCollisions(this.graph.getCell(model.attributes.parent)); ->>>>>>> 08c8e70578eaa5981dd06effa18dcbd7830e7ddd } else { children?.forEach(element => { diff --git a/client/src/main.css b/client/src/main.css index f6f7b20..0962ccb 100644 --- a/client/src/main.css +++ b/client/src/main.css @@ -971,6 +971,16 @@ video { color: rgb(59 130 246 / var(--tw-text-opacity)); } +.text-red-400 { + --tw-text-opacity: 1; + color: rgb(248 113 113 / var(--tw-text-opacity)); +} + +.text-red-500 { + --tw-text-opacity: 1; + color: rgb(239 68 68 / var(--tw-text-opacity)); +} + .underline { -webkit-text-decoration-line: underline; text-decoration-line: underline; diff --git a/client/src/views/Create/Create.jsx b/client/src/views/Create/Create.jsx index 6bacea1..5396fbb 100644 --- a/client/src/views/Create/Create.jsx +++ b/client/src/views/Create/Create.jsx @@ -13,6 +13,7 @@ export default function Create(props) { console.log('default name', getLocalGraphByID(id).name); const [graphName, setGraphName] = useState(getLocalGraphByID(id).name); const [eg, setExistentialGraph] = useState(null); + const [graphTool, setGraphTool] = useState(''); useEffect(() => { setExistentialGraph(new ExistentialGraph('main-paper', id)); @@ -33,6 +34,7 @@ export default function Create(props) { const handleSetGraphTool = (graphTool) => { console.log('set graph tool:', graphTool); eg.graphTool = graphTool; + setGraphTool(graphTool); } @@ -44,6 +46,7 @@ export default function Create(props) { handleGraphNameUpdate={handleGraphNameUpdate} handleSaveGraph={handleSaveGraph} handleSetGraphTool={handleSetGraphTool} + graphTool={graphTool} /> Date: Sat, 11 Nov 2023 16:33:55 -0500 Subject: [PATCH 17/35] troubleshooting shape lock Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- client/src/existential-graph/ExistentialGraph.js | 8 +++++++- client/src/existential-graph/GraphController.js | 2 +- client/src/existential-graph/shapes/Atomic.js | 4 ++-- client/src/existential-graph/shapes/Cut.js | 6 ++++-- client/src/main.css | 5 ----- 5 files changed, 14 insertions(+), 11 deletions(-) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index f26ff67..389b298 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -35,7 +35,8 @@ export default class ExistentialGraph { preventContextMenu: false, clickThreshold: 1, interactive: function(cellView) { - if (cellView.model.get("locked")) { + console.log('attr', cellView.model.attr('locked')) + if (cellView.model.attr("locked")) { return { //locking disables moving the element elementMove: false @@ -114,6 +115,10 @@ export default class ExistentialGraph { this.paper.on('cell:pointerdown', (cellView, evt, x, y) => { let cell = cellView.model; + if (cell.attr('locked') === true) { + console.log('this cell is locked!') + } + if (!cell.get('embeds') || cell.get('embeds').length === 0) { // Show the dragged element above all the other cells (except when the // element is a parent). @@ -363,6 +368,7 @@ export default class ExistentialGraph { this.sheet.deleteDoubleCut(this.selected_premise); } else if (this.graphTool === 'insert_subgraph') { + console.log('test') this.sheet.enableInsertMode(this.selected_premise); } else if (this.graphTool === 'erase_subgraph') { diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index 6bd93e1..7173c39 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -68,7 +68,6 @@ export default class GraphController { // sees on the paper let cellbbox = cell.getBoundingBox(); - console.log(this); let potential_parents = this.findPotentialParents(cellbbox); let parent = findSmallestCell(potential_parents); @@ -604,6 +603,7 @@ export default class GraphController { for (let cell of cells) { cell.lock() + console.log('cell', cell) } } diff --git a/client/src/existential-graph/shapes/Atomic.js b/client/src/existential-graph/shapes/Atomic.js index d370307..b069ae2 100644 --- a/client/src/existential-graph/shapes/Atomic.js +++ b/client/src/existential-graph/shapes/Atomic.js @@ -131,12 +131,12 @@ export default class Atomic extends joint.dia.Element { enableTools() { let elementView = this.findView(this.sheet.paper.paper); - this.showTools(); + elementView.showTools(); } disableTools() { let elementView = this.findView(this.sheet.paper.paper); - this.hideTools(); + elementView.hideTools(); } lock() { diff --git a/client/src/existential-graph/shapes/Cut.js b/client/src/existential-graph/shapes/Cut.js index 3fd7b49..0d43164 100644 --- a/client/src/existential-graph/shapes/Cut.js +++ b/client/src/existential-graph/shapes/Cut.js @@ -262,12 +262,14 @@ export default class Cut extends joint.dia.Element { } lock() { - this.set('locked', true) + console.log('locked') + this.attr('locked', true) this.disableTools() } unlock () { - this.set('locked', false) + console.log('unlocked') + this.attr('locked', false) this.enableTools() } diff --git a/client/src/main.css b/client/src/main.css index 0962ccb..56e41a5 100644 --- a/client/src/main.css +++ b/client/src/main.css @@ -976,11 +976,6 @@ video { color: rgb(248 113 113 / var(--tw-text-opacity)); } -.text-red-500 { - --tw-text-opacity: 1; - color: rgb(239 68 68 / var(--tw-text-opacity)); -} - .underline { -webkit-text-decoration-line: underline; text-decoration-line: underline; From 21922a199a70ec5b41aaadc8d77caea575e3e64b Mon Sep 17 00:00:00 2001 From: joekrystowski Date: Sat, 11 Nov 2023 17:16:49 -0500 Subject: [PATCH 18/35] fix locking bug --- client/src/existential-graph/ExistentialGraph.js | 15 ++++++++++++++- client/src/existential-graph/shapes/Atomic.js | 4 ++-- 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 389b298..063b8f1 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -45,6 +45,8 @@ export default class ExistentialGraph { return true; } }); + + console.log("JOINT PAPER ", this.paper) //default state on creation is NO_ACTION until the graph is initialized this.state = STATE.NO_ACTION; @@ -113,6 +115,7 @@ export default class ExistentialGraph { // First, unembed the cell that has just been grabbed by the user. this.paper.on('cell:pointerdown', (cellView, evt, x, y) => { + console.log("cell pointer down", this.paper) let cell = cellView.model; if (cell.attr('locked') === true) { @@ -400,7 +403,17 @@ export default class ExistentialGraph { this.sheet.addCut(config); } - this.paper.setInteractivity(true); + this.paper.setInteractivity( + function(cellView) { + console.log('attr', cellView.model.attr('locked')) + if (cellView.model.attr("locked")) { + return { + //locking disables moving the element + elementMove: false + } + }; + return true; + }); this.temp_cut = null; } diff --git a/client/src/existential-graph/shapes/Atomic.js b/client/src/existential-graph/shapes/Atomic.js index b069ae2..b3f26d0 100644 --- a/client/src/existential-graph/shapes/Atomic.js +++ b/client/src/existential-graph/shapes/Atomic.js @@ -140,12 +140,12 @@ export default class Atomic extends joint.dia.Element { } lock() { - this.set('locked', true) + this.attr('locked', true) this.disableTools() } unlock () { - this.set('locked', false) + this.attr('locked', false) this.enableTools() } From 15c9c495a6dc434d0306b741a6f1bca8cedd244b Mon Sep 17 00:00:00 2001 From: joekrystowski Date: Sat, 11 Nov 2023 17:26:02 -0500 Subject: [PATCH 19/35] Prevent embedding on locked elements Co-Authored-By: Eddie Krystowski --- client/src/existential-graph/GraphController.js | 4 ++++ client/src/existential-graph/shapes/Atomic.js | 4 ++++ client/src/existential-graph/shapes/Cut.js | 4 ++++ 3 files changed, 12 insertions(+) diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index 7173c39..392d57b 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -87,6 +87,10 @@ export default class GraphController { } else { let elements_inside = this.findElementsInside(cellbbox) for (const element of elements_inside) { + //do not add children to locked element + if (cell.isLocked()) { + break; + } if (element.get("parent") || element.id === cell.id) { continue; } diff --git a/client/src/existential-graph/shapes/Atomic.js b/client/src/existential-graph/shapes/Atomic.js index b3f26d0..0e84a38 100644 --- a/client/src/existential-graph/shapes/Atomic.js +++ b/client/src/existential-graph/shapes/Atomic.js @@ -149,6 +149,10 @@ export default class Atomic extends joint.dia.Element { this.enableTools() } + isLocked() { + return this.attr("locked") + } + setColor(color) { this.attr("rect/fill", color) } diff --git a/client/src/existential-graph/shapes/Cut.js b/client/src/existential-graph/shapes/Cut.js index 0d43164..f05d1e3 100644 --- a/client/src/existential-graph/shapes/Cut.js +++ b/client/src/existential-graph/shapes/Cut.js @@ -273,6 +273,10 @@ export default class Cut extends joint.dia.Element { this.enableTools() } + isLocked() { + return this.attr("locked") + } + } From 1a2a0926764011dbe68730877a69a07413621ac2 Mon Sep 17 00:00:00 2001 From: joekrystowski Date: Sat, 11 Nov 2023 18:35:05 -0500 Subject: [PATCH 20/35] stop destruction of locked elements --- client/src/existential-graph/shapes/Atomic.js | 8 +++++--- client/src/existential-graph/shapes/Cut.js | 1 + 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/client/src/existential-graph/shapes/Atomic.js b/client/src/existential-graph/shapes/Atomic.js index 0e84a38..9913fee 100644 --- a/client/src/existential-graph/shapes/Atomic.js +++ b/client/src/existential-graph/shapes/Atomic.js @@ -100,9 +100,11 @@ export default class Atomic extends joint.dia.Element { destroy() { - this.remove(); - //this.sheet.paper.handleDeleteCell(); - } + if (this.isLocked()) return; + + this.remove(); + //this.sheet.paper.handleDeleteCell(); + } obliterate() { this.destroy(); diff --git a/client/src/existential-graph/shapes/Cut.js b/client/src/existential-graph/shapes/Cut.js index f05d1e3..9eb8980 100644 --- a/client/src/existential-graph/shapes/Cut.js +++ b/client/src/existential-graph/shapes/Cut.js @@ -130,6 +130,7 @@ export default class Cut extends joint.dia.Element { } destroy() { + if (this.isLocked()) return; //check if cut has parents or children, if so children become new children of parent; let parent = this.getParentCell(); let children = this.getEmbeddedCells() From d3c919c106631f956b198a92ab76fb401fb68b90 Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Sat, 11 Nov 2023 18:44:48 -0500 Subject: [PATCH 21/35] Add behavior for deselecting graph tool, also add copy/paste graph tools Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- client/src/components/Toolbar/Toolbar.jsx | 24 +++++++++++++++---- .../src/existential-graph/ExistentialGraph.js | 12 ++++++++++ client/src/views/Create/Create.jsx | 5 ++++ 3 files changed, 36 insertions(+), 5 deletions(-) diff --git a/client/src/components/Toolbar/Toolbar.jsx b/client/src/components/Toolbar/Toolbar.jsx index b3709db..883f5c1 100644 --- a/client/src/components/Toolbar/Toolbar.jsx +++ b/client/src/components/Toolbar/Toolbar.jsx @@ -53,34 +53,48 @@ export default function Toolbar( props ) {
props.handleSetGraphTool('cut')} + onClick={() => props.graphTool === 'cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('cut')} > Cut props.handleSetGraphTool('insert_double_cut')} + onClick={() => props.graphTool === 'insert_double_cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('insert_double_cut')} > Insert Double Cut props.handleSetGraphTool('erase_double_cut')} + onClick={() => props.graphTool === 'erase_double_cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('erase_double_cut')} > Erase Double Cut props.handleSetGraphTool('insert_subgraph')} + onClick={() => props.graphTool === 'insert_subgraph' + ? props.handleSetGraphTool('auto_disable_insert') + : props.handleSetGraphTool('insert_subgraph')} > Insert Subgraph props.handleSetGraphTool('erase_subgraph')} + onClick={() => props.graphTool === 'erase_subgraph' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('erase_subgraph')} > Erase Subgraph + props.graphTool === 'copy_subgraph' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('copy_subgraph')} + > + Copy Subgraph + + props.graphTool === 'paste_subgraph' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('paste_subgraph')} + > + Paste Subgraph +
); diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 063b8f1..f5ca76e 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -74,6 +74,7 @@ export default class ExistentialGraph { // Name of action selected by toolbar graph tool buttons this.graphTool = null; + this.steps = []; this.initial_cut_pos = {x: 0, y: 0}; @@ -354,6 +355,7 @@ export default class ExistentialGraph { console.log('executing ', this.graphTool); if (this.graphTool === 'cut') { + this.steps.push('cut') let config = { position: this.getRelativeMousePos() } @@ -366,16 +368,26 @@ export default class ExistentialGraph { } else if (this.graphTool === 'insert_double_cut') { this.sheet.insertDoubleCut(this.selected_premise, this.getRelativeMousePos()) + this.steps.push('insert_double_cut') } else if (this.graphTool === 'erase_double_cut') { this.sheet.deleteDoubleCut(this.selected_premise); + this.steps.push('erase_double_cut') } else if (this.graphTool === 'insert_subgraph') { console.log('test') this.sheet.enableInsertMode(this.selected_premise); + this.steps.push('insert_subgraph') } else if (this.graphTool === 'erase_subgraph') { this.sheet.deleteSubgraph(this.selected_premise); + this.steps.push('erase_subgraph') + } + else if (this.graphTool === 'copy_subgraph') { + this.copySubgraph(this.selected_premise); + } + else if (this.graphTool === 'paste_subgraph') { + this.pasteSubgraph(this.selected_premise, this.getRelativeMousePos()); } diff --git a/client/src/views/Create/Create.jsx b/client/src/views/Create/Create.jsx index 5396fbb..532baab 100644 --- a/client/src/views/Create/Create.jsx +++ b/client/src/views/Create/Create.jsx @@ -32,6 +32,11 @@ export default function Create(props) { } const handleSetGraphTool = (graphTool) => { + if (graphTool === 'auto_disable_insert') { + graphTool = null; + eg.sheet.disableInsertMode(); + eg.steps.push('disable_insert_mode'); + } console.log('set graph tool:', graphTool); eg.graphTool = graphTool; setGraphTool(graphTool); From 68a72dc3c5c3b72161d9c6d846048091e078f6a9 Mon Sep 17 00:00:00 2001 From: joekrystowski Date: Sat, 11 Nov 2023 18:49:08 -0500 Subject: [PATCH 22/35] Add copy paste subgraph feature Co-Authored-By: Eddie Krystowski --- client/src/existential-graph/ExistentialGraph.js | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 063b8f1..435cd89 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -88,7 +88,8 @@ export default class ExistentialGraph { //default state after setup is CREATE mode this.state = STATE.CREATE; - + + this.clipboard = null } setPaperEvents(){ @@ -212,6 +213,16 @@ export default class ExistentialGraph { input.click(); } + copySubgraph(target) { + //save target root to clipboard + this.clipboard = target; + } + + pasteSubgraph(target, mouse_pos) { + if (this.clipboard === null) return; + this.sheet.addSubgraph(this.clipboard, mouse_pos, target) + } + addCellsInOrder(order) { console.log('adding in order', order) for (let [cellType, cell] of order) { From 08976fcbada03e19c9a118fd15c30919021ac27e Mon Sep 17 00:00:00 2001 From: joekrystowski Date: Sat, 11 Nov 2023 18:53:55 -0500 Subject: [PATCH 23/35] Use graph controller instead of sheet Co-Authored-By: Eddie Krystowski --- .../src/existential-graph/ExistentialGraph.js | 61 ++++++++----------- .../src/existential-graph/GraphController.js | 2 +- 2 files changed, 26 insertions(+), 37 deletions(-) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 435cd89..aac8f12 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -25,11 +25,11 @@ const PAPER_SIZE = { width: 4000, height: 4000 }; export default class ExistentialGraph { constructor(dom_id, graph_id) { console.log('LOADING GRAPH', graph_id) - this.sheet = new GraphController(this, graph_id); + this.graphController = new GraphController(this, graph_id); this.dom_element = document.getElementById(dom_id); this.paper = new joint.dia.Paper({ el: this.dom_element, - model: this.sheet.graph, + model: this.graphController.graph, width: PAPER_SIZE.width, height: PAPER_SIZE.height, preventContextMenu: false, @@ -130,10 +130,10 @@ export default class ExistentialGraph { } if (cell.get('parent')) { - this.sheet.graph.getCell(cell.get('parent')).unembed(cell); + this.graphController.graph.getCell(cell.get('parent')).unembed(cell); } cell.active(); - this.sheet.treeToFront(this.sheet.findRoot(cell)); + this.graphController.treeToFront(this.graphController.findRoot(cell)); }); // When the dragged cell is dropped over another cell, let it become a child of the @@ -142,22 +142,11 @@ export default class ExistentialGraph { let cell = cellView.model; - this.sheet.handleCollisions(cell) + this.graphController.handleCollisions(cell) cell.inactive(); - // if(!this.props.action) this.onGraphUpdate(); - // let nextAction; - // if (this.props.action) { - // nextAction = this.props.action(this.sheet, cell, this.getRelativeMousePos()); - // } - // if (this.props.handleClearAction && !nextAction) this.props.handleClearAction(); - // if(nextAction) this.props.handleActionChange(nextAction); this.selected_premise = null; }); - - // this.sheet.graph.on('add', () => { - // this.onGraphUpdate(); - // }); } @@ -197,7 +186,7 @@ export default class ExistentialGraph { const content = readerEvent.target.result; if (clear) { if (window.confirm("Erase your current workspace and import graph?")) { - this.sheet.graph.clear(); + this.graphController.graph.clear(); const dataObj = JSON.parse(content); const order = getSafeCellAddOrder(dataObj.cells); @@ -220,17 +209,17 @@ export default class ExistentialGraph { pasteSubgraph(target, mouse_pos) { if (this.clipboard === null) return; - this.sheet.addSubgraph(this.clipboard, mouse_pos, target) + this.graphController.addSubgraph(this.clipboard, mouse_pos, target); } addCellsInOrder(order) { console.log('adding in order', order) for (let [cellType, cell] of order) { if(cellType === 'cut') { - this.sheet.addCut(cell); + this.graphController.addCut(cell); } else if (cellType === 'atomic') { - this.sheet.addAtomic(cell); + this.graphController.addAtomic(cell); } } } @@ -253,9 +242,9 @@ export default class ExistentialGraph { exportGraphAsJSON() { // delete graph.changed; - let graphJSON = this.sheet.graph.toJSON(); + let graphJSON = this.graphController.graph.toJSON(); for(let i = 0; i < graphJSON.cells.length; i++) { - delete graphJSON.cells[i].sheet; + delete graphJSON.cells[i].graphController; } return graphJSON; @@ -300,8 +289,8 @@ export default class ExistentialGraph { console.log('created config', config) //eslint-disable-next-line //let new_rect = new Premise().create(config) - if (event.shiftKey) this.sheet.forcePremise(config); - else { this.sheet.addAtomic(config); } + if (event.shiftKey) this.graphController.forcePremise(config); + else { this.graphController.addAtomic(config); } this.canInsertPremise = false; this.previousPremiseCode = code; } @@ -313,16 +302,16 @@ export default class ExistentialGraph { } if (this.selected_premise) { config["child"] = this.selected_premise; - this.sheet.addCut(config); + this.graphController.addCut(config); } else { - this.sheet.addCut(config); + this.graphController.addCut(config); } } if (event.keyCode === 49) { //save template if (this.selected_premise) { - this.saved_template = this.sheet.graph.cloneSubgraph([this.selected_premise], {deep: true}); + this.saved_template = this.graphController.graph.cloneSubgraph([this.selected_premise], {deep: true}); } } @@ -330,7 +319,7 @@ export default class ExistentialGraph { const mouse_adjusted = this.getRelativeMousePos(); //console.log("position", mouse_adjusted) if (this.saved_template) { - this.sheet.addSubgraph(this.saved_template, mouse_adjusted, this.selected_premise); + this.graphController.addSubgraph(this.saved_template, mouse_adjusted, this.selected_premise); } } } @@ -352,7 +341,7 @@ export default class ExistentialGraph { } //this.temp_cut = new Cut().create(config); //this.history.current.lock(); - this.temp_cut = this.sheet.addCut(config); + this.temp_cut = this.graphController.addCut(config); this.temp_cut.active(); event.preventDefault(); console.log("CREATED TEMP CUT", this.temp_cut); @@ -370,23 +359,23 @@ export default class ExistentialGraph { } if (this.selected_premise) { config["child"] = this.selected_premise; - this.sheet.addCut(config); + this.graphController.addCut(config); } else { - this.sheet.addCut(config); + this.graphController.addCut(config); } } else if (this.graphTool === 'insert_double_cut') { - this.sheet.insertDoubleCut(this.selected_premise, this.getRelativeMousePos()) + this.graphController.insertDoubleCut(this.selected_premise, this.getRelativeMousePos()) } else if (this.graphTool === 'erase_double_cut') { - this.sheet.deleteDoubleCut(this.selected_premise); + this.graphController.deleteDoubleCut(this.selected_premise); } else if (this.graphTool === 'insert_subgraph') { console.log('test') - this.sheet.enableInsertMode(this.selected_premise); + this.graphController.enableInsertMode(this.selected_premise); } else if (this.graphTool === 'erase_subgraph') { - this.sheet.deleteSubgraph(this.selected_premise); + this.graphController.deleteSubgraph(this.selected_premise); } @@ -411,7 +400,7 @@ export default class ExistentialGraph { this.temp_cut.remove(); //this.history.current.unlock(); //NOTE: Temp cut must be deleted first or there will be uwnanted conflicts with collisions - this.sheet.addCut(config); + this.graphController.addCut(config); } this.paper.setInteractivity( diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index 392d57b..2c3cc42 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -294,7 +294,7 @@ export default class GraphController { } subgraphToGraph(node, clone, subgraph, parent=null) { - clone.sheet = this; + clone.graphController = this; clone.addTo(this.graph); if (parent != null) { parent.embed(clone); From 7d8aba9db3738d9b4811136ababa1367afd941d7 Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Fri, 17 Nov 2023 20:25:47 -0500 Subject: [PATCH 24/35] Enable real time collision resolution for temp cut Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- client/src/existential-graph/ExistentialGraph.js | 2 ++ client/src/views/Create/Create.jsx | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 13179ff..430977b 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -433,6 +433,8 @@ export default class ExistentialGraph { }); this.temp_cut.attr('rect/width', Math.abs(mouse_adjusted.x - this.initial_cut_pos.x)); this.temp_cut.attr('rect/height', Math.abs(mouse_adjusted.y - this.initial_cut_pos.y)); + this.graphController.handleCollisions(this.temp_cut) + this.graphController.cleanOverlaps() } } } \ No newline at end of file diff --git a/client/src/views/Create/Create.jsx b/client/src/views/Create/Create.jsx index 532baab..8a78892 100644 --- a/client/src/views/Create/Create.jsx +++ b/client/src/views/Create/Create.jsx @@ -34,7 +34,7 @@ export default function Create(props) { const handleSetGraphTool = (graphTool) => { if (graphTool === 'auto_disable_insert') { graphTool = null; - eg.sheet.disableInsertMode(); + eg.graphController.disableInsertMode(); eg.steps.push('disable_insert_mode'); } console.log('set graph tool:', graphTool); From 1e0e1ce0b058eb792fd3d1fef74190fe453713b5 Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Fri, 17 Nov 2023 22:45:43 -0500 Subject: [PATCH 25/35] Implement history class Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- .../src/existential-graph/ExistentialGraph.js | 3 + client/src/existential-graph/History.js | 23 --- client/src/existential-graph/Item.js | 10 - .../src/existential-graph/history/History.js | 187 ++++++++++++++++++ .../{ => history}/LinkedList.js | 2 +- 5 files changed, 191 insertions(+), 34 deletions(-) delete mode 100644 client/src/existential-graph/History.js delete mode 100644 client/src/existential-graph/Item.js create mode 100644 client/src/existential-graph/history/History.js rename client/src/existential-graph/{ => history}/LinkedList.js (94%) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index f5ca76e..f356315 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -4,6 +4,7 @@ import { getSafeCellAddOrder, getMousePosition, keyCodeIsActive, getMouseIsDown, import Cut from './shapes/Cut.js'; import $ from 'jquery'; import _ from 'lodash'; +import { History } from './history/History.js'; /** * @class Existential Graph @@ -45,6 +46,8 @@ export default class ExistentialGraph { return true; } }); + + this.history = new History(); console.log("JOINT PAPER ", this.paper) diff --git a/client/src/existential-graph/History.js b/client/src/existential-graph/History.js deleted file mode 100644 index 8dca939..0000000 --- a/client/src/existential-graph/History.js +++ /dev/null @@ -1,23 +0,0 @@ -import { LinkedList } from "./LinkedList"; - -/** - * A series of phyiscal changes to the graph. - */ - -class History { - constructor() { - this.history = new LinkedList(); - } - - undo() - { - // TODO - this.history.pop() - } - - do(action) - { - // TODO - this.history.push(action); - } -} \ No newline at end of file diff --git a/client/src/existential-graph/Item.js b/client/src/existential-graph/Item.js deleted file mode 100644 index 176e6df..0000000 --- a/client/src/existential-graph/Item.js +++ /dev/null @@ -1,10 +0,0 @@ - -export default class Item { - constructor(value = null) - { - this.prev = null; - this.next = null; - this.value = value; - } - -} \ No newline at end of file diff --git a/client/src/existential-graph/history/History.js b/client/src/existential-graph/history/History.js new file mode 100644 index 0000000..fca9e7d --- /dev/null +++ b/client/src/existential-graph/history/History.js @@ -0,0 +1,187 @@ +import React from "react"; + +/** + * This class manages and renders the timeline for the main workspace. + * See components/Paper/History/HistoryItems.jsx for the individual timeline components + */ +export default class History { + constructor(props) { + super(props); + + //if MAX_SIZE is exceeded, will start removing from bottom of stack + this.MAX_SIZE = 1024; + + // The idea of batch mode is to allow multiple premises/cuts to be added at once, + // but only count it as one HistoryItem on the timeline + // + // this.batch_mode simply toggles this behavior on and off, but should NOT be set directly. + // Instead, use this.startBatch() and this.endBatch(). + this.batch_mode = false; + // this.batch_state reflects the cells that were most recently pushed while batch_mode is true. + // Callling this.endBatch() will create a HistoryItem using this.batch_state cells. + // Never set this manually, use this.push(item) + this.batch_state = false; + + // if this.locked is true, no items will be able to be added to this.state.data, + // so no new HistoryItems can be created + this.locked = false; + + + this.state = { + //simple stack, each item is a collection of cells to be rendered by the paper + //of the respective HistoryItem component + data: [], + + //index represents the index of the current HistoryItem being viewed in the data array. + //For example, index = this.data.length - 1 is always the last thing you have done (present) + // index = 0 is always the first thing you have done (except for MAX_SIZE overflow) + index: 0 + } + } + + /** + * Call handler function on paper (passed through props) when multiple HistoryItems are + * skipped at a time (through clicking). + * @param {int} num index to jump to + */ + handleJump = (num) => { + this.state.index = num; + this.props.handleHistoryJump(this.getItem(num)); + } + + /** + * Clears the History timeline. + * @param {function} callback function to be executed after data has been emptied + */ + clear(callback) { + this.state = { + data: [], + index: 0 + }; + callback && callback(); + } + + + /** + * Adds collection of cells to data stack at the current index of the History timeline. + * + * Any entries after the current index will be erased since we only maintain one branch of history. + * + * If the size of the stack exceeds MAX_SIZE, the oldest entry will be deleted to make space. + * __RETURNS EARLY__ if this.locked is true. + * @param {*} item + * @returns + */ + push(item) { + if(this.locked) return; + + if(this.batch_mode) { + this.batch_state = item + return; + } + + //create a copy of state data (necessary since state must be immutable, can't change it directly) + const data = [...this.state.data]; + + // if we aren't on the last HistoryItem (the present/most recent) + if (this.state.index !== this.state.data.length - 1) { + //remove all states after current index + data.splice(this.state.index + 1); + } + + data.push(item); + + //remove from bottom of stack if we have more items than the max size allows + if (data.length >= this.MAX_SIZE) { + data.shift(); + } + + this.state.data = data; + this.state.index = data.length - 1; + } + + + /** + * Moves index of current HistoryItem to previous HistoryItem if there is one + * @returns HistoryItem at the previous index if undoing is allowed, false otherwise + */ + undo() { + let index = this.state.index; + if (this.state.index > 0) { + this.state.index = this.state.index - 1; + index -= 1; + return this.getItem(index); + } + return false; + } + + /** + * Moves index of current HistoryItem to subsequent HistoryItem if there is one + * @returns HistoryItem at the subsequent index if redoing is allowed, false otherwise + */ + redo() { + let index = this.state.index; + if (this.state.index < this.state.data.length - 1) { + this.state.index = this.state.index + 1; + index += 1; + return this.getItem(index); + } + return false; + } + + /** + * Gets a HistoryItem at a given index + * @param {int} index + * @returns HistoryItem at a given index if the index is valid, null otherwise + */ + getItem(index) { + if (index < 0 || index >= this.state.data.length) { + console.error(`ERROR: Tried to get HistoryItem this.state.data[${index}], index must be ${0} < ${index} <= ${this.state.data.length}`); + return null; + } + return this.state.data[index]; + } + + /** + * Locks the History so new HistoryItems cannot be added + */ + lock() { + this.locked = true; + } + + /** + * Unlocks the History so new HistoryItems can be added + */ + unlock() { + this.locked = false; + } + + /** + * Initializes a batch HistoryItem. + * + * Will make the History keep track of the most recent state sent to it through `this.push(item)` + * but will not actually update the History with that new item. + * + * `(see this.endBatch() for more info)` + */ + startBatch() { + this.batch_mode = true; + this.batch_state = null; + } + + /** + * Adds a batch HistoryItem to the History. + * + * Will take changes since `this.startBatch()` was called and add them to the History in one HistoryItem + */ + endBatch() { + this.batch_mode = false; + if (this.batch_state !== null) { + this.push(this.batch_state); + } + } + + render() { + return null; + } +} \ No newline at end of file diff --git a/client/src/existential-graph/LinkedList.js b/client/src/existential-graph/history/LinkedList.js similarity index 94% rename from client/src/existential-graph/LinkedList.js rename to client/src/existential-graph/history/LinkedList.js index 9c947d3..a1a65c1 100644 --- a/client/src/existential-graph/LinkedList.js +++ b/client/src/existential-graph/history/LinkedList.js @@ -1,4 +1,4 @@ -import Item from "./Item"; +import Item from "./HistoryItem"; export class LinkedList { constructor() { From 9df9780369c016823ddb22f6ac1d48154da6b54c Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Fri, 17 Nov 2023 23:13:36 -0500 Subject: [PATCH 26/35] initialize history on EG and implement undo/redo Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- .../src/existential-graph/ExistentialGraph.js | 39 +++++++++++++++++-- .../src/existential-graph/history/History.js | 7 ++-- 2 files changed, 39 insertions(+), 7 deletions(-) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 4e25fd6..74ffdf7 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -4,7 +4,7 @@ import { getSafeCellAddOrder, getMousePosition, keyCodeIsActive, getMouseIsDown, import Cut from './shapes/Cut.js'; import $ from 'jquery'; import _ from 'lodash'; -import { History } from './history/History.js'; +import History from './history/History.js'; /** * @class Existential Graph @@ -55,8 +55,11 @@ export default class ExistentialGraph { this.state = STATE.NO_ACTION; //console.log(getLocalGraphByID(graph_id)) - const order = getSafeCellAddOrder(getLocalGraphByID(graph_id).graphJSON.cells); + const loadedGraphData = getLocalGraphByID(graph_id).graphJSON.cells; + const order = getSafeCellAddOrder(loadedGraphData); this.addCellsInOrder(order); + + this.history.push(loadedGraphData); // Paper events are callback functions defined on the joint paper that are // triggered by user input (i.e. keystrokes, clicking, dragging, etc) @@ -120,7 +123,7 @@ export default class ExistentialGraph { // First, unembed the cell that has just been grabbed by the user. this.paper.on('cell:pointerdown', (cellView, evt, x, y) => { - console.log("cell pointer down", this.paper) + //console.log("cell pointer down", this.paper) let cell = cellView.model; if (cell.attr('locked') === true) { @@ -151,6 +154,36 @@ export default class ExistentialGraph { this.selected_premise = null; }); + + this.graphController.graph.on('change', (cell, opt) => { + const cells = this.graphController.graph.getCells(); + this.history.push(cells); + }); + + //PAPER UNDO AND REDO EVENTS + $(this.dom_element).on('keydown', (event) => { + if (event.keyCode === 90 && (event.ctrlKey || event.metaKey) && !event.shiftKey) { + const new_state = this.history.current.undo(); + this.selected_premise = null; + //only update graph if new state exists + //undo will return false if can't undo anymore + if (new_state) { + this.history.current.lock(); + this.sheet.importCells(new_state); + this.history.current.unlock(); + } + } + if (event.keyCode === 90 && (event.ctrlKey || event.metaKey) && event.shiftKey) { + const new_state = this.history.current.redo(); + //only update graph if new state exists + //redo will return false if can't redo anymore + if (new_state) { + this.history.current.lock(); + this.sheet.importCells(new_state); + this.history.current.unlock(); + } + } + }); } diff --git a/client/src/existential-graph/history/History.js b/client/src/existential-graph/history/History.js index fca9e7d..8df283e 100644 --- a/client/src/existential-graph/history/History.js +++ b/client/src/existential-graph/history/History.js @@ -5,8 +5,7 @@ import React from "react"; * See components/Paper/History/HistoryItems.jsx for the individual timeline components */ export default class History { - constructor(props) { - super(props); + constructor() { //if MAX_SIZE is exceeded, will start removing from bottom of stack this.MAX_SIZE = 1024; @@ -40,13 +39,13 @@ export default class History { } /** - * Call handler function on paper (passed through props) when multiple HistoryItems are + * Call handler function on paper (passed through) when multiple HistoryItems are * skipped at a time (through clicking). * @param {int} num index to jump to */ handleJump = (num) => { this.state.index = num; - this.props.handleHistoryJump(this.getItem(num)); + //this.props.handleHistoryJump(this.getItem(num)); } /** From 61d02d163f7863ca169b9b1d4dd2c2de620901b5 Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Fri, 17 Nov 2023 23:20:19 -0500 Subject: [PATCH 27/35] update hypergraph after rule application Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- client/src/existential-graph/ExistentialGraph.js | 10 +++++++++- client/src/existential-graph/ExistentialHypergraph.js | 4 ++-- client/src/existential-graph/GraphController.js | 1 + client/src/views/Create/Create.jsx | 4 +++- 4 files changed, 15 insertions(+), 4 deletions(-) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 74ffdf7..6f35feb 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -24,7 +24,7 @@ const STATE = { const PAPER_SIZE = { width: 4000, height: 4000 }; export default class ExistentialGraph { - constructor(dom_id, graph_id) { + constructor(dom_id, graph_id, hypergraph) { console.log('LOADING GRAPH', graph_id) this.graphController = new GraphController(this, graph_id); this.dom_element = document.getElementById(dom_id); @@ -48,6 +48,7 @@ export default class ExistentialGraph { }); this.history = new History(); + this.hypergraph = hypergraph; console.log("JOINT PAPER ", this.paper) @@ -401,25 +402,32 @@ export default class ExistentialGraph { } else { this.graphController.addCut(config); } + this.hypergraph.addStep(this.graphController.graph_id, 'cut', this.graphController.graph.getCells()); } else if (this.graphTool === 'insert_double_cut') { this.graphController.insertDoubleCut(this.selected_premise, this.getRelativeMousePos()) + this.hypergraph.addStep(this.graphController.graph_id, 'insert_double_cut', this.graphController.graph.getCells()); } else if (this.graphTool === 'erase_double_cut') { this.graphController.deleteDoubleCut(this.selected_premise); + this.hypergraph.addStep(this.graphController.graph_id, 'erase_double_cut', this.graphController.graph.getCells()); } else if (this.graphTool === 'insert_subgraph') { console.log('test') this.graphController.enableInsertMode(this.selected_premise); + this.hypergraph.addStep(this.graphController.graph_id, 'insert_subgraph', this.graphController.graph.getCells()); } else if (this.graphTool === 'erase_subgraph') { this.graphController.deleteSubgraph(this.selected_premise); + this.hypergraph.addStep(this.graphController.graph_id, 'erase_subgraph', this.graphController.graph.getCells()); } else if (this.graphTool === 'copy_subgraph') { this.copySubgraph(this.selected_premise); + this.hypergraph.addStep(this.graphController.graph_id, 'copy_subgraph', this.graphController.graph.getCells()); } else if (this.graphTool === 'paste_subgraph') { this.pasteSubgraph(this.selected_premise, this.getRelativeMousePos()); + this.hypergraph.addStep(this.graphController.graph_id, 'paste_subgraph', this.graphController.graph.getCells()); } this.graphTool = null; diff --git a/client/src/existential-graph/ExistentialHypergraph.js b/client/src/existential-graph/ExistentialHypergraph.js index 56657f6..8c63cc0 100644 --- a/client/src/existential-graph/ExistentialHypergraph.js +++ b/client/src/existential-graph/ExistentialHypergraph.js @@ -1,4 +1,4 @@ -import { Queue } from "./LinkedList" +import { Queue } from "./history/LinkedList" /** * Existential Hypergraphs are directed graphs in which the nodes represent Existential Graphs and the edges represent applications @@ -6,7 +6,7 @@ import { Queue } from "./LinkedList" * * We represent proofs using Existential Hypergraphs */ -class ExistentialHypergraph { +export default class ExistentialHypergraph { constructor(rootGraph) { this.root = rootGraph; diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index 2c3cc42..fa21ec4 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -23,6 +23,7 @@ const DISABLED_BACKGROUND_COLORS = { export default class GraphController { constructor(parent_paper, graph_id) { this.paper = parent_paper; + this.graph_id = graph_id; const graphData = getLocalGraphByID(graph_id); console.log(graphData); diff --git a/client/src/views/Create/Create.jsx b/client/src/views/Create/Create.jsx index 8a78892..3dff5db 100644 --- a/client/src/views/Create/Create.jsx +++ b/client/src/views/Create/Create.jsx @@ -4,6 +4,7 @@ import { useParams } from 'react-router-dom'; import Toolbar from '@components/Toolbar/Toolbar.jsx'; import { CreatePaperComponent } from '@components/Paper'; import ExistentialGraph from '../../existential-graph/ExistentialGraph'; +import ExistentialHypergraph from '../../existential-graph/ExistentialHypergraph'; import { addToLocalGraphData, getLocalGraphByID } from '../../util/util'; @@ -12,11 +13,12 @@ export default function Create(props) { const { id } = useParams(); console.log('default name', getLocalGraphByID(id).name); const [graphName, setGraphName] = useState(getLocalGraphByID(id).name); + const [existentialHypergraph, setExistentialHypergraph] = useState(new ExistentialHypergraph()); const [eg, setExistentialGraph] = useState(null); const [graphTool, setGraphTool] = useState(''); useEffect(() => { - setExistentialGraph(new ExistentialGraph('main-paper', id)); + setExistentialGraph(new ExistentialGraph('main-paper', id, existentialHypergraph)); }, [id]); From 5d8e6cde917b7d34cacae43605a4a20d7f5a6665 Mon Sep 17 00:00:00 2001 From: joekrystowski Date: Fri, 17 Nov 2023 23:22:01 -0500 Subject: [PATCH 28/35] rename paper member variable to new naming conventions --- client/src/existential-graph/GraphController.js | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index fa21ec4..ff6cca7 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -22,7 +22,7 @@ const DISABLED_BACKGROUND_COLORS = { export default class GraphController { constructor(parent_paper, graph_id) { - this.paper = parent_paper; + this.existential_graph = parent_paper; this.graph_id = graph_id; const graphData = getLocalGraphByID(graph_id); @@ -472,7 +472,7 @@ export default class GraphController { // returns cell under mouse with the highest z value; getCellAtMouse() { //console.log("mouse pos", this.paper.getRelativeMousePos()); - const mouse_pos = this.paper.getRelativeMousePos() + const mouse_pos = this.existential_graph.getRelativeMousePos() const cells = this.graph.getCells().filter(cell => mouse_pos.x <= cell.attributes.position.x + cell.attributes.attrs.rect.width && mouse_pos.x >= cell.attributes.position.x && mouse_pos.y <= cell.attributes.position.y + cell.attributes.attrs.rect.height From d1f4fe3b1a91e12c9bb1b9ad801135955babf024 Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Fri, 24 Nov 2023 15:18:20 -0500 Subject: [PATCH 29/35] proofs wip Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- client/src/components/Toolbar/Toolbar.jsx | 18 ++++++++-- .../ExistentialHypergraph.js | 1 - .../ExistentialHypergraphNode.js | 2 +- .../existential-graph/history/LinkedList.js | 30 ---------------- client/src/existential-graph/shapes/Atomic.js | 14 ++++---- client/src/existential-graph/shapes/Cut.js | 34 +++++++++---------- client/src/main.css | 21 ++++++++++++ client/src/views/Create/Create.jsx | 15 ++++++++ 8 files changed, 76 insertions(+), 59 deletions(-) delete mode 100644 client/src/existential-graph/history/LinkedList.js diff --git a/client/src/components/Toolbar/Toolbar.jsx b/client/src/components/Toolbar/Toolbar.jsx index 883f5c1..11b5923 100644 --- a/client/src/components/Toolbar/Toolbar.jsx +++ b/client/src/components/Toolbar/Toolbar.jsx @@ -12,11 +12,15 @@ export default function Toolbar( props ) { if (!e.target.value) e.target.value = "Untitled Graph"; props.handleGraphNameUpdate(e.target.value); } + + function handleStartProofClicked() { + props.handleStartProofClicked(); + } return ( -
+
{/* Left-side file management tools */} -
+
{/* Graph tools */} -
+
props.graphTool === 'cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('cut')} @@ -96,6 +100,14 @@ export default function Toolbar( props ) { Paste Subgraph
+ + +
); } \ No newline at end of file diff --git a/client/src/existential-graph/ExistentialHypergraph.js b/client/src/existential-graph/ExistentialHypergraph.js index 8c63cc0..51e8373 100644 --- a/client/src/existential-graph/ExistentialHypergraph.js +++ b/client/src/existential-graph/ExistentialHypergraph.js @@ -1,4 +1,3 @@ -import { Queue } from "./history/LinkedList" /** * Existential Hypergraphs are directed graphs in which the nodes represent Existential Graphs and the edges represent applications diff --git a/client/src/existential-graph/ExistentialHypergraphNode.js b/client/src/existential-graph/ExistentialHypergraphNode.js index 99e0f31..3f8ec39 100644 --- a/client/src/existential-graph/ExistentialHypergraphNode.js +++ b/client/src/existential-graph/ExistentialHypergraphNode.js @@ -2,7 +2,7 @@ export default class ExistentialHypergraphNode { constructor(existentialGraph) { - this.value = existentialGraph; + this.existentialGraph = existentialGraph; this.parent = null; this.next = []; diff --git a/client/src/existential-graph/history/LinkedList.js b/client/src/existential-graph/history/LinkedList.js deleted file mode 100644 index a1a65c1..0000000 --- a/client/src/existential-graph/history/LinkedList.js +++ /dev/null @@ -1,30 +0,0 @@ -import Item from "./HistoryItem"; - -export class LinkedList { - constructor() { - this.head = new Item("head") - this.tail = new Item("tail"); - this.head.next = this.tail; - this.tail.prev = this.head; - } - - pop() { - let element = this.tail.prev; - this.tail.prev = element.prev; - return this.element.value; - } - - push(val) { - let new_item = new Item(val); - - new_item.prev = this.tail.prev; - new_item.next = this.tail; - - this.tail.prev.next = new_item; - this.tail.prev = new_item; - } - - peek() { - return this.tail.prev.value() - } -} \ No newline at end of file diff --git a/client/src/existential-graph/shapes/Atomic.js b/client/src/existential-graph/shapes/Atomic.js index 9913fee..bac827b 100644 --- a/client/src/existential-graph/shapes/Atomic.js +++ b/client/src/existential-graph/shapes/Atomic.js @@ -55,7 +55,7 @@ export default class Atomic extends joint.dia.Element { }] //custom constructor for shape, should more or less always use this over the default constructor - create(config, sheet, fast) { + create(config, graphController, fast) { const options = _.cloneDeep(ATOMIC_DEFAULTS); if (config) { @@ -64,7 +64,7 @@ export default class Atomic extends joint.dia.Element { options.attrs.rect = Object.assign(options.attrs.rect, config.attrs && config.attrs.rect); options.attrs.text = Object.assign(options.attrs.text, config.attrs && config.attrs.text); } - options.sheet = sheet; + options.graphController = graphController; const premise = new Atomic({ markup: '', @@ -87,9 +87,9 @@ export default class Atomic extends joint.dia.Element { }); //have to set this out here since we actually do want a reference to this object, not a copy - premise.sheet = options.sheet; + premise.graphController = options.graphController; - premise.addTo(premise.sheet.graph) + premise.addTo(premise.graphController.graph) console.log('added ?') //add tools (some events events also) @@ -132,12 +132,12 @@ export default class Atomic extends joint.dia.Element { } enableTools() { - let elementView = this.findView(this.sheet.paper.paper); + let elementView = this.findView(this.graphController.paper.paper); elementView.showTools(); } disableTools() { - let elementView = this.findView(this.sheet.paper.paper); + let elementView = this.findView(this.graphController.paper.paper); elementView.hideTools(); } @@ -162,7 +162,7 @@ export default class Atomic extends joint.dia.Element { //TODO: see Cut.addTools() addTools(element) { //element view is in charge of rendering the elements on the paper - let elementView = element.findView(element.sheet.paper.paper); + let elementView = element.findView(element.graphController.existential_graph.paper); //clear any old tools elementView.removeTools(); // boundary tool shows boundaries of element diff --git a/client/src/existential-graph/shapes/Cut.js b/client/src/existential-graph/shapes/Cut.js index 9eb8980..6c46675 100644 --- a/client/src/existential-graph/shapes/Cut.js +++ b/client/src/existential-graph/shapes/Cut.js @@ -58,7 +58,7 @@ export default class Cut extends joint.dia.Element { }] //custom constructor for shape, should more or less always use this over the default constructor - create(config, sheet) { + create(config, graphController) { const options = _.cloneDeep(CUT_DEFAULTS); if (config) { options.position = Object.assign(options.position, config.position); @@ -66,7 +66,7 @@ export default class Cut extends joint.dia.Element { options.attrs.rect = Object.assign(options.attrs.rect, config.attrs && config.attrs.rect); options.attrs.text = Object.assign(options.attrs.text, config.attrs && config.attrs.text); } - options.sheet = sheet; + options.graphController = graphController; // adjust size / position if cut was created with a child // in order for undo/redo to function properly @@ -98,13 +98,13 @@ export default class Cut extends joint.dia.Element { level: 0 }, // set custom attributes here: - sheet: options.sheet + graphController: options.graphController }); //have to set this out here since we actually do want a reference to this object, not a copy - cut.sheet = options.sheet; + cut.graphController = options.graphController; - cut.addTo(cut.sheet.graph); + cut.addTo(cut.graphController.graph); //add tools (some events events also) this.addTools(cut); //let audio = new Audio(Snip); @@ -114,7 +114,7 @@ export default class Cut extends joint.dia.Element { let child = config.child; let hasparent = false; if (child.get("parent")) { - let parent = cut.sheet.graph.getCell(child.get("parent")); + let parent = cut.graphController.graph.getCell(child.get("parent")); parent.unembed(child); parent.embed(cut) parent.toBack() @@ -122,7 +122,7 @@ export default class Cut extends joint.dia.Element { } cut.embed(child) if (hasparent) { - cut.sheet.treeResize(cut, cut.attributes.attrs.rect.width / 2); + cut.graphController.treeResize(cut, cut.attributes.attrs.rect.width / 2); } } //console.log(cut); @@ -139,7 +139,7 @@ export default class Cut extends joint.dia.Element { } this.remove(); if (parent) { - this.sheet.handleCollisions(parent); + this.graphController.handleCollisions(parent); } //this.sheet.paper.handleDeleteCell(); @@ -148,19 +148,19 @@ export default class Cut extends joint.dia.Element { obliterate() { // If non-empty cell, destroy all children let children = this.attributes.embeds; - if (children) children.forEach(child => {this.sheet.graph.getCell(child).obliterate()}); + if (children) children.forEach(child => {this.graphController.graph.getCell(child).obliterate()}); // Then destroy self this.destroy(); } active() { //cut is being interacted with (ie grabbing, dragging or moving etc) - this.sheet.colorByLevel(this, {even:color.shapes.background.even.active, odd:color.shapes.background.odd.active, premise: color.shapes.background.default.color}); + this.graphController.colorByLevel(this, {even:color.shapes.background.even.active, odd:color.shapes.background.odd.active, premise: color.shapes.background.default.color}); } inactive() { //cut is not being interacted with (ie grabbing, dragging or moving etc) - this.sheet.colorByLevel(this, {even:color.shapes.background.even.inactive, odd:color.shapes.background.odd.inactive, premise: color.shapes.background.default.color}); + this.graphController.colorByLevel(this, {even:color.shapes.background.even.inactive, odd:color.shapes.background.odd.inactive, premise: color.shapes.background.default.color}); } getBoundingBox() { @@ -204,7 +204,7 @@ export default class Cut extends joint.dia.Element { /// ( i think we can? ) addTools(element) { //element view is in charge of rendering the elements on the paper - let elementView = element.findView(element.sheet.paper.paper); + let elementView = element.findView(element.graphController.existential_graph.paper); //clear any old tools elementView.removeTools(); // boundary tool shows boundaries of element @@ -253,12 +253,12 @@ export default class Cut extends joint.dia.Element { } enableTools() { - let elementView = this.findView(this.sheet.paper.paper); + let elementView = this.findView(this.graphController.paper.paper); elementView.showTools(); } disableTools() { - let elementView = this.findView(this.sheet.paper.paper); + let elementView = this.findView(this.graphController.paper.paper); elementView.hideTools(); } @@ -314,7 +314,7 @@ const MIN_SIZE = { * @param {MouseEvent} event */ function resize_mousedown(event) { - const target = this.sheet.graph.getCell($(event.target).parent().attr('model-id')); + const target = this.graphController.graph.getCell($(event.target).parent().attr('model-id')); prev_pos = { x: event.clientX, y: event.clientY @@ -325,7 +325,7 @@ function resize_mousedown(event) { event.stopPropagation(); if (target.get('parent')) { - this.sheet.graph.getCell(target.get('parent')).unembed(target); + this.graphController.graph.getCell(target.get('parent')).unembed(target); } } @@ -421,7 +421,7 @@ function resize_mousemove(event) { function resize_mouseup (event) { $(document).off('mouseup', resize_mouseup); $(document).off('mousemove', resize_mousemove); - event.data.target.sheet.handleCollisions(event.data.target); + event.data.target.graphController.handleCollisions(event.data.target); //event.data.target.sheet.paper.onGraphUpdate(); } diff --git a/client/src/main.css b/client/src/main.css index 56e41a5..e421d24 100644 --- a/client/src/main.css +++ b/client/src/main.css @@ -601,6 +601,14 @@ video { margin-right: 1rem; } +.mr-8 { + margin-right: 2rem; +} + +.mb-2 { + margin-bottom: 0.5rem; +} + .inline-block { display: inline-block; } @@ -868,10 +876,23 @@ video { padding-right: 0.25rem; } +.px-12 { + padding-left: 3rem; + padding-right: 3rem; +} + .pt-2 { padding-top: 0.5rem; } +.pl-2 { + padding-left: 0.5rem; +} + +.pr-12 { + padding-right: 3rem; +} + .text-left { text-align: left; } diff --git a/client/src/views/Create/Create.jsx b/client/src/views/Create/Create.jsx index 3dff5db..eb32723 100644 --- a/client/src/views/Create/Create.jsx +++ b/client/src/views/Create/Create.jsx @@ -16,11 +16,18 @@ export default function Create(props) { const [existentialHypergraph, setExistentialHypergraph] = useState(new ExistentialHypergraph()); const [eg, setExistentialGraph] = useState(null); const [graphTool, setGraphTool] = useState(''); + const [inProof, setInProof] = useState(false) useEffect(() => { setExistentialGraph(new ExistentialGraph('main-paper', id, existentialHypergraph)); }, [id]); + useEffect(() => { + if (inProof) { + console.log('proof successfully started'); + setExistentialHypergraph(new ExistentialHypergraph(eg)); + } + }, [inProof]); const handleSaveGraph = () => { console.log('CREATE VIEW SAVING GRAPH', graphName, id); @@ -44,6 +51,13 @@ export default function Create(props) { setGraphTool(graphTool); } + const handleStartProofClicked = () => { + console.log('starting proof for graph ' + id); + if (!inProof) { + setInProof(true); + } + } + return (
@@ -53,6 +67,7 @@ export default function Create(props) { handleGraphNameUpdate={handleGraphNameUpdate} handleSaveGraph={handleSaveGraph} handleSetGraphTool={handleSetGraphTool} + handleStartProofClicked={handleStartProofClicked} graphTool={graphTool} /> Date: Mon, 27 Nov 2023 19:07:51 -0500 Subject: [PATCH 30/35] proof mode updates Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- .../src/existential-graph/ExistentialGraph.js | 22 ++++++--- .../ExistentialHypergraph.js | 24 +++++---- .../ExistentialHypergraphNode.js | 5 +- .../src/existential-graph/GraphController.js | 39 +++++++++++++-- client/src/main.css | 49 +++++++------------ client/src/views/Create/Create.jsx | 10 ++++ 6 files changed, 95 insertions(+), 54 deletions(-) diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 6f35feb..2efcba3 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -28,6 +28,7 @@ export default class ExistentialGraph { console.log('LOADING GRAPH', graph_id) this.graphController = new GraphController(this, graph_id); this.dom_element = document.getElementById(dom_id); + this.id = graph_id; this.paper = new joint.dia.Paper({ el: this.dom_element, model: this.graphController.graph, @@ -49,6 +50,7 @@ export default class ExistentialGraph { this.history = new History(); this.hypergraph = hypergraph; + this.proofMode = false; console.log("JOINT PAPER ", this.paper) @@ -389,8 +391,7 @@ export default class ExistentialGraph { onMouseUp = () => { if (this.graphTool) { - console.log('executing ', this.graphTool); - + console.log('executing ', this.graphTool); if (this.graphTool === 'cut') { this.steps.push('cut') let config = { @@ -406,31 +407,36 @@ export default class ExistentialGraph { } else if (this.graphTool === 'insert_double_cut') { this.graphController.insertDoubleCut(this.selected_premise, this.getRelativeMousePos()) - this.hypergraph.addStep(this.graphController.graph_id, 'insert_double_cut', this.graphController.graph.getCells()); + if (this.proofMode) this.hypergraph.addStep(this.graphController.graph_id, 'insert_double_cut', this.graphController.graph.getCells()); } else if (this.graphTool === 'erase_double_cut') { + if (!this.selected_premise) return; this.graphController.deleteDoubleCut(this.selected_premise); - this.hypergraph.addStep(this.graphController.graph_id, 'erase_double_cut', this.graphController.graph.getCells()); + if (this.proofMode) this.hypergraph.addStep(this.graphController.graph_id, 'erase_double_cut', this.graphController.graph.getCells()); } else if (this.graphTool === 'insert_subgraph') { console.log('test') this.graphController.enableInsertMode(this.selected_premise); - this.hypergraph.addStep(this.graphController.graph_id, 'insert_subgraph', this.graphController.graph.getCells()); + if (this.proofMode) this.hypergraph.addStep(this.graphController.graph_id, 'insert_subgraph', this.graphController.graph.getCells()); } else if (this.graphTool === 'erase_subgraph') { this.graphController.deleteSubgraph(this.selected_premise); - this.hypergraph.addStep(this.graphController.graph_id, 'erase_subgraph', this.graphController.graph.getCells()); + if (this.proofMode) this.hypergraph.addStep(this.graphController.graph_id, 'erase_subgraph', this.graphController.graph.getCells()); } else if (this.graphTool === 'copy_subgraph') { this.copySubgraph(this.selected_premise); - this.hypergraph.addStep(this.graphController.graph_id, 'copy_subgraph', this.graphController.graph.getCells()); + if (this.proofMode) this.hypergraph.addStep(this.graphController.graph_id, 'copy_subgraph', this.graphController.graph.getCells()); } else if (this.graphTool === 'paste_subgraph') { this.pasteSubgraph(this.selected_premise, this.getRelativeMousePos()); - this.hypergraph.addStep(this.graphController.graph_id, 'paste_subgraph', this.graphController.graph.getCells()); + if (this.proofMode) this.hypergraph.addStep(this.graphController.graph_id, 'paste_subgraph', this.graphController.graph.getCells()); } this.graphTool = null; + + this.onGraphToolUse && this.onGraphToolUse(); + + console.log('hypergraph', this.hypergraph) return } diff --git a/client/src/existential-graph/ExistentialHypergraph.js b/client/src/existential-graph/ExistentialHypergraph.js index 51e8373..30316e9 100644 --- a/client/src/existential-graph/ExistentialHypergraph.js +++ b/client/src/existential-graph/ExistentialHypergraph.js @@ -1,4 +1,7 @@ +import ExistentialHypergraphNode from "./ExistentialHypergraphNode"; + + /** * Existential Hypergraphs are directed graphs in which the nodes represent Existential Graphs and the edges represent applications * of logical rules to transition from one graph to another. @@ -8,23 +11,26 @@ export default class ExistentialHypergraph { constructor(rootGraph) { - this.root = rootGraph; + this.root = new ExistentialHypergraphNode(rootGraph); + this.ptr = this.root; } addStep(graphId, rule, destination) { - const hypergraphNode = this.find(graphId); - if (hypergraphNode) - hypergraphNode.addTransition(rule, destination); + //const hypergraphNode = this.find(graphId); + //if (hypergraphNode) { + this.ptr = this.ptr.addTransition(rule, destination); + ////} } find(graphId) { - const current = [this.root] + let current = [this.root] while(current.length > 0) { let next = [] - for (let graph of current) { - if (graph.id === graphId) - return graph; - next.push(...graph.next); + for (let node of current) { + console.log('searching node...', node) + if (node.existentialGraph.id === graphId) + return node; + next.push(...node.next); } current = next; diff --git a/client/src/existential-graph/ExistentialHypergraphNode.js b/client/src/existential-graph/ExistentialHypergraphNode.js index 3f8ec39..35d8310 100644 --- a/client/src/existential-graph/ExistentialHypergraphNode.js +++ b/client/src/existential-graph/ExistentialHypergraphNode.js @@ -9,10 +9,13 @@ export default class ExistentialHypergraphNode { } addTransition(rule, destination) { + const destinationNode = new ExistentialHypergraphNode(destination); this.next.push({ rule, - destination: new ExistentialHypergraphNode(destination) + destination: destinationNode }); + + return destinationNode; } diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index ff6cca7..b5bdce9 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -61,6 +61,31 @@ export default class GraphController { return cut; } + // embedInCut(config, collisions=true, selected=null) { + // const cut = this.addCut(config, collisions=false) + // alert("bortnite") + // let parent = null; + // if (selected.get('parent')) { + // parent = selected.getParentCell(); + // } + // if (selected !== null) { + // if (parent) { + // parent.unembed(selected); + // parent.embed(cut) + // } + // cut.embed(selected) + // } + + // if (parent) this.pack(parent) + // this.pack(cut) + + // // Play snip sound + // //let snip = new Audio(Snip); + // //this.handlePlayAudio(snip); + // //this.paper.onGraphUpdate(); + // return cut; + // } + handleCollisions(cell, clean=true) { //console.log("=================== HANDLE COLLISIONS =========================") //This function takes a Cell as input and, using its position @@ -739,12 +764,16 @@ export default class GraphController { } new_cuts[0].embed(new_cuts[1]) this.colorByLevel(new_cuts[0]) - let selected_premise = this.paper.selected_premise; + let selected_premise = this.existential_graph.selected_premise; if (selected_premise && selected_premise.attributes.type === "dia.Element.Cut") { - selected_premise.embed(new_cuts[0]); - this.colorByLevel(selected_premise) - this.pack(selected_premise) - } + selected_premise.embed(new_cuts[0]); + this.colorByLevel(selected_premise) + this.pack(selected_premise) + }// else + // { + // new_cuts[1].embed(selected_premise) + // this.pack(selected_premise) + // } this.handleCollisions(new_cuts[0]) } diff --git a/client/src/main.css b/client/src/main.css index e421d24..93cb87a 100644 --- a/client/src/main.css +++ b/client/src/main.css @@ -589,6 +589,10 @@ video { margin-right: 5rem; } +.mb-2 { + margin-bottom: 0.5rem; +} + .mt-10 { margin-top: 2.5rem; } @@ -601,14 +605,6 @@ video { margin-right: 1rem; } -.mr-8 { - margin-right: 2rem; -} - -.mb-2 { - margin-bottom: 0.5rem; -} - .inline-block { display: inline-block; } @@ -659,15 +655,6 @@ video { width: 2.5rem; } -.w-1\/4 { - width: 25%; -} - -.w-max { - width: -webkit-max-content; - width: max-content; -} - .w-4\/5 { width: 80%; } @@ -688,6 +675,11 @@ video { width: 8rem; } +.w-max { + width: -webkit-max-content; + width: max-content; +} + .min-w-\[2rem\] { min-width: 2rem; } @@ -815,6 +807,11 @@ video { background-color: transparent; } +.bg-slate-400 { + --tw-bg-opacity: 1; + background-color: rgb(148 163 184 / var(--tw-bg-opacity)); +} + .bg-blue-500 { --tw-bg-opacity: 1; background-color: rgb(59 130 246 / var(--tw-bg-opacity)); @@ -825,11 +822,6 @@ video { background-color: rgb(22 163 74 / var(--tw-bg-opacity)); } -.bg-slate-400 { - --tw-bg-opacity: 1; - background-color: rgb(148 163 184 / var(--tw-bg-opacity)); -} - .bg-slate-600 { --tw-bg-opacity: 1; background-color: rgb(71 85 105 / var(--tw-bg-opacity)); @@ -876,15 +868,6 @@ video { padding-right: 0.25rem; } -.px-12 { - padding-left: 3rem; - padding-right: 3rem; -} - -.pt-2 { - padding-top: 0.5rem; -} - .pl-2 { padding-left: 0.5rem; } @@ -893,6 +876,10 @@ video { padding-right: 3rem; } +.pt-2 { + padding-top: 0.5rem; +} + .text-left { text-align: left; } diff --git a/client/src/views/Create/Create.jsx b/client/src/views/Create/Create.jsx index eb32723..d916565 100644 --- a/client/src/views/Create/Create.jsx +++ b/client/src/views/Create/Create.jsx @@ -29,6 +29,12 @@ export default function Create(props) { } }, [inProof]); + useEffect(() => { + console.log('new hypergraph', existentialHypergraph) + console.log('eg', eg) + if (eg) eg.hypergraph = existentialHypergraph; + }, [existentialHypergraph]) + const handleSaveGraph = () => { console.log('CREATE VIEW SAVING GRAPH', graphName, id); const graphJSON = eg.exportGraphAsJSON(); @@ -49,12 +55,16 @@ export default function Create(props) { console.log('set graph tool:', graphTool); eg.graphTool = graphTool; setGraphTool(graphTool); + eg.onGraphToolUse = () => { + setGraphTool(null); + } } const handleStartProofClicked = () => { console.log('starting proof for graph ' + id); if (!inProof) { setInProof(true); + eg.proofMode = true; } } From 547089762bbacd44a76fde00bdef6b2e615fb531 Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Mon, 27 Nov 2023 20:14:28 -0500 Subject: [PATCH 31/35] basic ui for proof view and update graph tool custom drawn images Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- client/src/assets/images/addcut.png | Bin 0 -> 207 bytes client/src/assets/images/copysubgraph.png | Bin 0 -> 296 bytes client/src/assets/images/insertdoublecut.png | Bin 0 -> 250 bytes client/src/assets/images/insertsubgraph.png | Bin 0 -> 269 bytes client/src/assets/images/pastesubgraph.png | Bin 0 -> 268 bytes client/src/assets/images/removedoublecut.png | Bin 0 -> 279 bytes client/src/assets/images/removesubgraph.png | Bin 0 -> 268 bytes client/src/components/App/App.jsx | 19 +++-- client/src/components/Header/Header.jsx | 14 +++- .../components/Paper/ProofView/ProofView.jsx | 32 +++++++++ .../Toolbar/GraphTool/GraphTool.jsx | 30 +++++++- client/src/existential-graph/shapes/Atomic.js | 4 +- client/src/existential-graph/shapes/Cut.js | 4 +- client/src/main.css | 67 ++++++++++++++++++ client/src/views/Create/Create.jsx | 21 ++++-- 15 files changed, 175 insertions(+), 16 deletions(-) create mode 100644 client/src/assets/images/addcut.png create mode 100644 client/src/assets/images/copysubgraph.png create mode 100644 client/src/assets/images/insertdoublecut.png create mode 100644 client/src/assets/images/insertsubgraph.png create mode 100644 client/src/assets/images/pastesubgraph.png create mode 100644 client/src/assets/images/removedoublecut.png create mode 100644 client/src/assets/images/removesubgraph.png create mode 100644 client/src/components/Paper/ProofView/ProofView.jsx diff --git a/client/src/assets/images/addcut.png b/client/src/assets/images/addcut.png new file mode 100644 index 0000000000000000000000000000000000000000..66aa4ff7217ee64bf34e1882045e5d139fa244fb GIT binary patch literal 207 zcmeAS@N?(olHy`uVBq!ia0vp^3LwnE1|*BCs=fdz#^NA%Cx&(BWL^R}`JOJ0ArY;~ z2@j7%UFdM(P~-N4Iu^(_zq0v;AE3Ea^NeA zVUUuQNaL^I;Mu{vLWuQ5gM*$#FViB1SnorO{EdO^Jyr=<7#H(NlrpSy(_B0I+2RC| t1B?vG4Pu&4gZvKwt>#OO@J#ddWzYh$Ie-`hE(K2pQJ$`TF6*2UngD0KII92v literal 0 HcmV?d00001 diff --git a/client/src/assets/images/copysubgraph.png b/client/src/assets/images/copysubgraph.png new file mode 100644 index 0000000000000000000000000000000000000000..54054bb823d1c7cdc4d77b569c38ddc4627f2efe GIT binary patch literal 296 zcmeAS@N?(olHy`uVBq!ia0vp^3LwnE1|*BCs=fdz#^NA%Cx&(BWL^R}Cp=voLn2z= zhF|15tiaQgT(9+8>*n^j_^1w{wVBG>H_D1QdKb+)-Kmtaq?X0fzLmknMXu$D=nIy4 z*HZL$#7_FI{dL+Z*2xFt7Dy)wWlZi|xK*!lcIWbqUd)%5yNf^kE_i~qb^&Gg+(svo{KUSa8H5WgT8ARaP}*+^L4 nn&X&h5zv)CAMa^W&3q*!{7vNPh8@h(4Xh8EJQoXn;%eaTZ_r?R(sa*l>g0>kO+AUd z77j}zHZ!>Wn{bvdB`~(=K&0jY;|tM`{yTi+oEO_)keJJ!^~F^4fBAw^y(6+W7^E9~ z4zBsjkif{kX>FVdQ I&MBb@096oS9{>OV literal 0 HcmV?d00001 diff --git a/client/src/assets/images/pastesubgraph.png b/client/src/assets/images/pastesubgraph.png new file mode 100644 index 0000000000000000000000000000000000000000..ba253e1fe817d95c405dc8ea291bcf70a31e8e6a GIT binary patch literal 268 zcmeAS@N?(olHy`uVBq!ia0vp^3LwnE1|*BCs=fdz#^NA%Cx&(BWL^R}Ydl>XLn2z= zPW9$%P~dT4f9%`4+-RPtxx literal 0 HcmV?d00001 diff --git a/client/src/assets/images/removedoublecut.png b/client/src/assets/images/removedoublecut.png new file mode 100644 index 0000000000000000000000000000000000000000..c2abb5c29448949e7590a4b6c631cff1f06166b6 GIT binary patch literal 279 zcmeAS@N?(olHy`uVBq!ia0vp^3LwnE1|*BCs=fdz#^NA%Cx&(BWL^R}+dW+zLn2z= zPCv-opupqWU8s~+=#!qPx@X188(}=H^$+8FI{sb15T?MSJ?A>lw|0gUrA4d>e*|O_ zLXTDJdTOwnFccOoKC(ckLF=vIJ^6bTvP! zTCOD;YftF!oTg~L#;~0ILQw)oLrMhmL#BYVJz$|f}~Q0Wj)T;auFUUfnMNCjqptK^<~fkvN?bl S1TFXLn2z= zPQS?8pupqOU8t0n=#!SH`e!4j*`g3Hzs~Q;PY&;kS>G$r`1D&k+x2#a6s1M10Y4Um z%DKF6-z6AS^z`>{nFP;EaaZTGT7O_(!MN!A&7zbP0 Hl+XkK(yw5p literal 0 HcmV?d00001 diff --git a/client/src/components/App/App.jsx b/client/src/components/App/App.jsx index 58128ea..60c5cab 100644 --- a/client/src/components/App/App.jsx +++ b/client/src/components/App/App.jsx @@ -12,12 +12,17 @@ import Login from '../../views/Login/Login'; import $ from 'jquery'; import Signup from '../../views/Signup/Signup'; +const GRAPH_STATE = { + CREATE: 0, + PROOF: 1 +} export default function App(props) { const workspace = useRef(null); const [muted, setMuted] = useState(true); const [sound, setSound] = useState(null); + const [graphState, setGraphState] = useState(GRAPH_STATE.CREATE); //initial render useEffect(() => { @@ -54,6 +59,10 @@ export default function App(props) { audio.play(); } + const handleGraphStateChange = (newGraphState) => { + setGraphState(newGraphState); + } + /* const getGraphForExport = () => { return workspace.current.mainPaper.current.sheet.graph; @@ -84,17 +93,17 @@ export default function App(props) { return (
-
+
} /> - } /> - + } /> + {/* + } /> */} } /> diff --git a/client/src/components/Header/Header.jsx b/client/src/components/Header/Header.jsx index a1e7351..3b48381 100644 --- a/client/src/components/Header/Header.jsx +++ b/client/src/components/Header/Header.jsx @@ -3,6 +3,12 @@ import { Link } from "react-router-dom"; import Navbar from "@components/Header/Navbar/Navbar"; import Profile from "@components/Header/Profile/Profile"; import eg_logo from "@assets/images/eg_logo.png"; + +const GRAPH_STATE = { + CREATE: 0, + PROOF: 1 +} + /** * Component for Header of Existential Graphs. * @@ -19,7 +25,13 @@ export default function Header( props ) { className=" w-10 flex-item m-2 mr-20" /> - + + {/* */} +
+

+ {props.graphState === GRAPH_STATE.CREATE ? 'Create' : 'Proof'} Mode +

+
diff --git a/client/src/components/Paper/ProofView/ProofView.jsx b/client/src/components/Paper/ProofView/ProofView.jsx new file mode 100644 index 0000000..f0c1d26 --- /dev/null +++ b/client/src/components/Paper/ProofView/ProofView.jsx @@ -0,0 +1,32 @@ +import { useState } from "react" + +export default function ProofView(props) { + + const [expanded, setExpanded] = useState(false); + + const handleToggleExpand = () => { + setExpanded(!expanded); + } + + return ( +
+ { + props.show && + + } + + { + props.show && expanded && +
+ } + +
+ ) +} \ No newline at end of file diff --git a/client/src/components/Toolbar/GraphTool/GraphTool.jsx b/client/src/components/Toolbar/GraphTool/GraphTool.jsx index 20b9125..b0be77f 100644 --- a/client/src/components/Toolbar/GraphTool/GraphTool.jsx +++ b/client/src/components/Toolbar/GraphTool/GraphTool.jsx @@ -1,10 +1,38 @@ import React from 'react'; +import addCutPng from "@assets/images/addcut.png"; +import insertDoubleCutPng from "@assets/images/insertdoublecut.png"; +import removeDoubleCutPng from "@assets/images/removedoublecut.png"; +import insertSubgraphPng from "@assets/images/insertsubgraph.png"; +import removeSubgraphPng from "@assets/images/removesubgraph.png"; +import copySubgraphPng from "@assets/images/copysubgraph.png" +import pasteSubgraphPng from "@assets/images/pastesubgraph.png" + +const imageMap = { + 'Cut': addCutPng, + 'Insert Double Cut' : insertDoubleCutPng, + 'Erase Double Cut' : removeDoubleCutPng, + 'Insert Subgraph' : insertSubgraphPng, + 'Erase Subgraph' : removeSubgraphPng, + 'Copy Subgraph' : copySubgraphPng, + 'Paste Subgraph' : pasteSubgraphPng +}; + +/** + * Insert Double Cut +Erase Double Cut +Insert Subgraph +Erase Subgraph +Copy Subgraph +Paste Subgraph + */ + export default function GraphTool(props) { return (
- {props.children}
diff --git a/client/src/existential-graph/shapes/Atomic.js b/client/src/existential-graph/shapes/Atomic.js index bac827b..a96ff98 100644 --- a/client/src/existential-graph/shapes/Atomic.js +++ b/client/src/existential-graph/shapes/Atomic.js @@ -132,12 +132,12 @@ export default class Atomic extends joint.dia.Element { } enableTools() { - let elementView = this.findView(this.graphController.paper.paper); + let elementView = this.findView(this.graphController.existential_graph.paper); elementView.showTools(); } disableTools() { - let elementView = this.findView(this.graphController.paper.paper); + let elementView = this.findView(this.graphController.existential_graph.paper); elementView.hideTools(); } diff --git a/client/src/existential-graph/shapes/Cut.js b/client/src/existential-graph/shapes/Cut.js index 6c46675..8ba7e9e 100644 --- a/client/src/existential-graph/shapes/Cut.js +++ b/client/src/existential-graph/shapes/Cut.js @@ -253,12 +253,12 @@ export default class Cut extends joint.dia.Element { } enableTools() { - let elementView = this.findView(this.graphController.paper.paper); + let elementView = this.findView(this.graphController.existential_graph.paper); elementView.showTools(); } disableTools() { - let elementView = this.findView(this.graphController.paper.paper); + let elementView = this.findView(this.graphController.existential_graph.paper); elementView.hideTools(); } diff --git a/client/src/main.css b/client/src/main.css index 93cb87a..da12d92 100644 --- a/client/src/main.css +++ b/client/src/main.css @@ -569,6 +569,18 @@ video { right: 0px; } +.top-0 { + top: 0px; +} + +.right-10 { + right: 2.5rem; +} + +.top-8 { + top: 2rem; +} + .z-10 { z-index: 10; } @@ -680,6 +692,10 @@ video { width: max-content; } +.w-96 { + width: 24rem; +} + .min-w-\[2rem\] { min-width: 2rem; } @@ -729,6 +745,10 @@ video { flex-direction: column; } +.items-start { + align-items: flex-start; +} + .items-center { align-items: center; } @@ -760,6 +780,10 @@ video { border-color: rgb(243 244 246 / var(--tw-divide-opacity)); } +.self-end { + align-self: flex-end; +} + .self-center { align-self: center; } @@ -780,10 +804,18 @@ video { border-radius: 9999px; } +.border-2 { + border-width: 2px; +} + .border-b-2 { border-bottom-width: 2px; } +.border-solid { + border-style: solid; +} + .border-none { border-style: none; } @@ -793,6 +825,16 @@ video { border-color: rgb(0 0 0 / var(--tw-border-opacity)); } +.border-indigo-600 { + --tw-border-opacity: 1; + border-color: rgb(79 70 229 / var(--tw-border-opacity)); +} + +.border-slate-600 { + --tw-border-opacity: 1; + border-color: rgb(71 85 105 / var(--tw-border-opacity)); +} + .bg-white { --tw-bg-opacity: 1; background-color: rgb(255 255 255 / var(--tw-bg-opacity)); @@ -827,6 +869,11 @@ video { background-color: rgb(71 85 105 / var(--tw-bg-opacity)); } +.bg-slate-300 { + --tw-bg-opacity: 1; + background-color: rgb(203 213 225 / var(--tw-bg-opacity)); +} + .p-5 { padding: 1.25rem; } @@ -868,6 +915,16 @@ video { padding-right: 0.25rem; } +.px-3 { + padding-left: 0.75rem; + padding-right: 0.75rem; +} + +.py-3 { + padding-top: 0.75rem; + padding-bottom: 0.75rem; +} + .pl-2 { padding-left: 0.5rem; } @@ -934,6 +991,11 @@ video { line-height: 2.25rem; } +.text-lg { + font-size: 1.125rem; + line-height: 1.75rem; +} + .font-medium { font-weight: 500; } @@ -1127,6 +1189,11 @@ html, body, #root, .app { background-color: rgb(241 245 249 / var(--tw-bg-opacity)); } +.hover\:bg-slate-200:hover { + --tw-bg-opacity: 1; + background-color: rgb(226 232 240 / var(--tw-bg-opacity)); +} + .hover\:text-slate-600:hover { --tw-text-opacity: 1; color: rgb(71 85 105 / var(--tw-text-opacity)); diff --git a/client/src/views/Create/Create.jsx b/client/src/views/Create/Create.jsx index d916565..da4aad7 100644 --- a/client/src/views/Create/Create.jsx +++ b/client/src/views/Create/Create.jsx @@ -7,6 +7,12 @@ import ExistentialGraph from '../../existential-graph/ExistentialGraph'; import ExistentialHypergraph from '../../existential-graph/ExistentialHypergraph'; import { addToLocalGraphData, getLocalGraphByID } from '../../util/util'; +import ProofView from '../../components/Paper/ProofView/ProofView'; + +const GRAPH_STATE = { + CREATE: 0, + PROOF: 1 +} export default function Create(props) { @@ -65,6 +71,7 @@ export default function Create(props) { if (!inProof) { setInProof(true); eg.proofMode = true; + props.handleGraphStateChange(GRAPH_STATE.PROOF); } } @@ -80,11 +87,15 @@ export default function Create(props) { handleStartProofClicked={handleStartProofClicked} graphTool={graphTool} /> - +
+ + +
+ ); } \ No newline at end of file From 8766be63cfbe688be54067aea22a31e39b596cd5 Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Mon, 27 Nov 2023 21:33:12 -0500 Subject: [PATCH 32/35] Add proof tools, separate graph and proof tools on toolbar, convert hypergraph to array Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- client/src/assets/images/deiteration.png | Bin 0 -> 292 bytes client/src/assets/images/iteration.png | Bin 0 -> 245 bytes .../components/Paper/ProofView/ProofStep.jsx | 18 +++ .../components/Paper/ProofView/ProofView.jsx | 30 +++- .../Toolbar/GraphTool/GraphTool.jsx | 14 +- client/src/components/Toolbar/Toolbar.jsx | 97 ++++++++++- .../ExistentialHypergraph.js | 21 +++ .../ExistentialHypergraphNode.js | 2 + client/src/main.css | 153 ++++++++++++++++++ client/src/views/Create/Create.jsx | 3 +- 10 files changed, 327 insertions(+), 11 deletions(-) create mode 100644 client/src/assets/images/deiteration.png create mode 100644 client/src/assets/images/iteration.png create mode 100644 client/src/components/Paper/ProofView/ProofStep.jsx diff --git a/client/src/assets/images/deiteration.png b/client/src/assets/images/deiteration.png new file mode 100644 index 0000000000000000000000000000000000000000..8e471710333eccabcdeec280fafef03f97e44565 GIT binary patch literal 292 zcmeAS@N?(olHy`uVBq!ia0vp^3LwnE1|*BCs=fdz#^NA%Cx&(BWL^R}M?75|Ln2z= zPP@z7pup3@|Jdc+qZ#K8d3{~!Cb-ZfcU9+o=_Lmr|5E0x^$=K`_Q@vZkd46Xp8dXy znRexzF7m!Ut61y%^*Q~gXDoYAQ;_?2%k^djjU%_-T5n`&@R6O+p^8%6GAo!h+pajmF2*Tj4R81T z*sY9hG2d58h5EI2m`OKw%sEvMk{?{aEO&spf}x_}Df`549&OSSOl0aOdP*PSby@WB z&JMG+KiV0W1uv~rPx0}|NnCJK{Lk?->*9hQu-P!!IBe$J8oG;V2creQEtkx~yg7`5 iKnL=rMtG+A`Z8z%*&IL&0+)g(gD6i|KbLh*2~7Y1pit5P literal 0 HcmV?d00001 diff --git a/client/src/components/Paper/ProofView/ProofStep.jsx b/client/src/components/Paper/ProofView/ProofStep.jsx new file mode 100644 index 0000000..b00e02d --- /dev/null +++ b/client/src/components/Paper/ProofView/ProofStep.jsx @@ -0,0 +1,18 @@ + +const ruleMap = { + 'Start': 'Proof Start', + 'insert_double_cut': 'Insert Double Cut', + 'erase_double_cut': 'Erase Double Cut', + 'insert_subgraph': 'Insert Subgraph', + 'erase_subgraph': 'Erase Subgraph', + 'copy_subgraph': 'Copy Subgraph', + 'paste_subgraph': 'Paste Subgraph' +} + +export default function ProofStep(props) { + return ( +
+ { ruleMap[props.rule] || '???'} +
+ ) +} \ No newline at end of file diff --git a/client/src/components/Paper/ProofView/ProofView.jsx b/client/src/components/Paper/ProofView/ProofView.jsx index f0c1d26..f154c9d 100644 --- a/client/src/components/Paper/ProofView/ProofView.jsx +++ b/client/src/components/Paper/ProofView/ProofView.jsx @@ -1,8 +1,9 @@ import { useState } from "react" +import ProofStep from "./ProofStep"; export default function ProofView(props) { - const [expanded, setExpanded] = useState(false); + const [expanded, setExpanded] = useState(true); const handleToggleExpand = () => { setExpanded(!expanded); @@ -14,7 +15,7 @@ export default function ProofView(props) { props.show &&
diff --git a/client/src/components/Toolbar/GraphTool/GraphTool.jsx b/client/src/components/Toolbar/GraphTool/GraphTool.jsx index b0be77f..a198008 100644 --- a/client/src/components/Toolbar/GraphTool/GraphTool.jsx +++ b/client/src/components/Toolbar/GraphTool/GraphTool.jsx @@ -5,8 +5,10 @@ import insertDoubleCutPng from "@assets/images/insertdoublecut.png"; import removeDoubleCutPng from "@assets/images/removedoublecut.png"; import insertSubgraphPng from "@assets/images/insertsubgraph.png"; import removeSubgraphPng from "@assets/images/removesubgraph.png"; -import copySubgraphPng from "@assets/images/copysubgraph.png" -import pasteSubgraphPng from "@assets/images/pastesubgraph.png" +import copySubgraphPng from "@assets/images/copysubgraph.png"; +import pasteSubgraphPng from "@assets/images/pastesubgraph.png"; +import iterationPng from '@assets/images/iteration.png'; +import deiterationPng from '@assets/images/deiteration.png'; const imageMap = { 'Cut': addCutPng, @@ -15,7 +17,9 @@ const imageMap = { 'Insert Subgraph' : insertSubgraphPng, 'Erase Subgraph' : removeSubgraphPng, 'Copy Subgraph' : copySubgraphPng, - 'Paste Subgraph' : pasteSubgraphPng + 'Paste Subgraph' : pasteSubgraphPng, + 'Iteration' : iterationPng, + 'Deiteration' : deiterationPng }; /** @@ -30,8 +34,8 @@ Paste Subgraph export default function GraphTool(props) { return ( -
- {props.children} diff --git a/client/src/components/Toolbar/Toolbar.jsx b/client/src/components/Toolbar/Toolbar.jsx index 11b5923..7787b6a 100644 --- a/client/src/components/Toolbar/Toolbar.jsx +++ b/client/src/components/Toolbar/Toolbar.jsx @@ -54,7 +54,7 @@ export default function Toolbar( props ) {
{/* Graph tools */} -
+
props.graphTool === 'cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('cut')} @@ -99,11 +99,104 @@ export default function Toolbar( props ) { > Paste Subgraph + + { + props.inProof && +
+ Graph + Tools +
+ } + + { + props.inProof && +
+ } + + { + props.inProof && +
+ Proof + Steps +
+ } + + + {/** + * + * + * Proof steps + * + */} + + { + props.inProof && + props.graphTool === 'insert_double_cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('insert_double_cut')} + > + Insert Double Cut + + } + + { + props.inProof && + props.graphTool === 'erase_double_cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('erase_double_cut')} + > + Erase Double Cut + + } + + { + props.inProof && + props.graphTool === 'insert_subgraph' + ? props.handleSetGraphTool('auto_disable_insert') + : props.handleSetGraphTool('insert_subgraph')} + > + Insert Subgraph + + } + + { + props.inProof && + props.graphTool === 'erase_subgraph' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('erase_subgraph')} + > + Erase Subgraph + + } + + + { + props.inProof && + props.graphTool === 'iteration' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('iteration')} + > + Iteration + + } + + { + props.inProof && + props.graphTool === 'deiteration' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('deiteration')} + > + Deiteration + + } +
From 379171be86bc8a8326932e0aed87cb497d37b5af Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Mon, 27 Nov 2023 21:40:39 -0500 Subject: [PATCH 33/35] Only update hypergraph if using proof tool Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- client/src/components/Toolbar/Toolbar.jsx | 16 +++++++++------- client/src/existential-graph/ExistentialGraph.js | 16 +++++++++------- client/src/views/Create/Create.jsx | 9 ++++++++- 3 files changed, 26 insertions(+), 15 deletions(-) diff --git a/client/src/components/Toolbar/Toolbar.jsx b/client/src/components/Toolbar/Toolbar.jsx index 7787b6a..cee8210 100644 --- a/client/src/components/Toolbar/Toolbar.jsx +++ b/client/src/components/Toolbar/Toolbar.jsx @@ -16,6 +16,8 @@ export default function Toolbar( props ) { function handleStartProofClicked() { props.handleStartProofClicked(); } + + return (
@@ -133,7 +135,7 @@ export default function Toolbar( props ) { props.inProof && props.graphTool === 'insert_double_cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('insert_double_cut')} + onClick={() => props.graphTool === 'insert_double_cut' ? props.handleSetProofTool(null) : props.handleSetProofTool('insert_double_cut')} > Insert Double Cut @@ -143,7 +145,7 @@ export default function Toolbar( props ) { props.inProof && props.graphTool === 'erase_double_cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('erase_double_cut')} + onClick={() => props.graphTool === 'erase_double_cut' ? props.handleSetProofTool(null) : props.handleSetProofTool('erase_double_cut')} > Erase Double Cut @@ -154,8 +156,8 @@ export default function Toolbar( props ) { props.graphTool === 'insert_subgraph' - ? props.handleSetGraphTool('auto_disable_insert') - : props.handleSetGraphTool('insert_subgraph')} + ? props.handleSetProofTool('auto_disable_insert') + : props.handleSetProofTool('insert_subgraph')} > Insert Subgraph @@ -165,7 +167,7 @@ export default function Toolbar( props ) { props.inProof && props.graphTool === 'erase_subgraph' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('erase_subgraph')} + onClick={() => props.graphTool === 'erase_subgraph' ? props.handleSetProofTool(null) : props.handleSetProofTool('erase_subgraph')} > Erase Subgraph @@ -176,7 +178,7 @@ export default function Toolbar( props ) { props.inProof && props.graphTool === 'iteration' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('iteration')} + onClick={() => props.graphTool === 'iteration' ? props.handleSetProofTool(null) : props.handleSetProofTool('iteration')} > Iteration @@ -186,7 +188,7 @@ export default function Toolbar( props ) { props.inProof && props.graphTool === 'deiteration' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('deiteration')} + onClick={() => props.graphTool === 'deiteration' ? props.handleSetProofTool(null) : props.handleSetProofTool('deiteration')} > Deiteration diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 2efcba3..92e197f 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -51,6 +51,7 @@ export default class ExistentialGraph { this.history = new History(); this.hypergraph = hypergraph; this.proofMode = false; + this.isProofTool = false; console.log("JOINT PAPER ", this.paper) @@ -403,33 +404,34 @@ export default class ExistentialGraph { } else { this.graphController.addCut(config); } - this.hypergraph.addStep(this.graphController.graph_id, 'cut', this.graphController.graph.getCells()); + + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'cut', this.graphController.graph.getCells()); } else if (this.graphTool === 'insert_double_cut') { this.graphController.insertDoubleCut(this.selected_premise, this.getRelativeMousePos()) - if (this.proofMode) this.hypergraph.addStep(this.graphController.graph_id, 'insert_double_cut', this.graphController.graph.getCells()); + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'insert_double_cut', this.graphController.graph.getCells()); } else if (this.graphTool === 'erase_double_cut') { if (!this.selected_premise) return; this.graphController.deleteDoubleCut(this.selected_premise); - if (this.proofMode) this.hypergraph.addStep(this.graphController.graph_id, 'erase_double_cut', this.graphController.graph.getCells()); + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'erase_double_cut', this.graphController.graph.getCells()); } else if (this.graphTool === 'insert_subgraph') { console.log('test') this.graphController.enableInsertMode(this.selected_premise); - if (this.proofMode) this.hypergraph.addStep(this.graphController.graph_id, 'insert_subgraph', this.graphController.graph.getCells()); + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'insert_subgraph', this.graphController.graph.getCells()); } else if (this.graphTool === 'erase_subgraph') { this.graphController.deleteSubgraph(this.selected_premise); - if (this.proofMode) this.hypergraph.addStep(this.graphController.graph_id, 'erase_subgraph', this.graphController.graph.getCells()); + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'erase_subgraph', this.graphController.graph.getCells()); } else if (this.graphTool === 'copy_subgraph') { this.copySubgraph(this.selected_premise); - if (this.proofMode) this.hypergraph.addStep(this.graphController.graph_id, 'copy_subgraph', this.graphController.graph.getCells()); + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'copy_subgraph', this.graphController.graph.getCells()); } else if (this.graphTool === 'paste_subgraph') { this.pasteSubgraph(this.selected_premise, this.getRelativeMousePos()); - if (this.proofMode) this.hypergraph.addStep(this.graphController.graph_id, 'paste_subgraph', this.graphController.graph.getCells()); + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'paste_subgraph', this.graphController.graph.getCells()); } this.graphTool = null; diff --git a/client/src/views/Create/Create.jsx b/client/src/views/Create/Create.jsx index bdcf261..bcdb0f3 100644 --- a/client/src/views/Create/Create.jsx +++ b/client/src/views/Create/Create.jsx @@ -52,7 +52,7 @@ export default function Create(props) { setGraphName(newName); } - const handleSetGraphTool = (graphTool) => { + const handleSetGraphTool = (graphTool, isProofTool=false) => { if (graphTool === 'auto_disable_insert') { graphTool = null; eg.graphController.disableInsertMode(); @@ -60,12 +60,18 @@ export default function Create(props) { } console.log('set graph tool:', graphTool); eg.graphTool = graphTool; + eg.isProofTool = isProofTool; setGraphTool(graphTool); eg.onGraphToolUse = () => { setGraphTool(null); + eg.isProofTool = false; } } + const handleSetProofTool = (graphTool) => { + handleSetGraphTool(graphTool, true); + } + const handleStartProofClicked = () => { console.log('starting proof for graph ' + id); if (!inProof) { @@ -84,6 +90,7 @@ export default function Create(props) { handleGraphNameUpdate={handleGraphNameUpdate} handleSaveGraph={handleSaveGraph} handleSetGraphTool={handleSetGraphTool} + handleSetProofTool={handleSetProofTool} handleStartProofClicked={handleStartProofClicked} graphTool={graphTool} inProof={inProof} From aa14bf60de2c12fd8ce648ab1eb7b2bd83ada0c8 Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Mon, 27 Nov 2023 22:38:17 -0500 Subject: [PATCH 34/35] enable auto execute for iteration and deiteration Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- .../components/Paper/ProofView/ProofStep.jsx | 4 ++- .../components/Paper/ProofView/ProofView.jsx | 6 +++++ .../Toolbar/GraphTool/GraphTool.jsx | 10 ++++++-- client/src/components/Toolbar/Toolbar.jsx | 2 ++ .../src/existential-graph/ExistentialGraph.js | 2 -- client/src/main.css | 25 +++++++++++++++++++ client/src/views/Create/Create.jsx | 20 ++++++++++++++- 7 files changed, 63 insertions(+), 6 deletions(-) diff --git a/client/src/components/Paper/ProofView/ProofStep.jsx b/client/src/components/Paper/ProofView/ProofStep.jsx index b00e02d..7acd2d6 100644 --- a/client/src/components/Paper/ProofView/ProofStep.jsx +++ b/client/src/components/Paper/ProofView/ProofStep.jsx @@ -6,7 +6,9 @@ const ruleMap = { 'insert_subgraph': 'Insert Subgraph', 'erase_subgraph': 'Erase Subgraph', 'copy_subgraph': 'Copy Subgraph', - 'paste_subgraph': 'Paste Subgraph' + 'paste_subgraph': 'Paste Subgraph', + 'iteration': 'Iteration', + 'deiteration': 'Deiteration' } export default function ProofStep(props) { diff --git a/client/src/components/Paper/ProofView/ProofView.jsx b/client/src/components/Paper/ProofView/ProofView.jsx index f154c9d..83560b8 100644 --- a/client/src/components/Paper/ProofView/ProofView.jsx +++ b/client/src/components/Paper/ProofView/ProofView.jsx @@ -1,6 +1,8 @@ import { useState } from "react" import ProofStep from "./ProofStep"; + + export default function ProofView(props) { const [expanded, setExpanded] = useState(true); @@ -9,6 +11,10 @@ export default function ProofView(props) { setExpanded(!expanded); } + + + + return (
{ diff --git a/client/src/components/Toolbar/GraphTool/GraphTool.jsx b/client/src/components/Toolbar/GraphTool/GraphTool.jsx index a198008..a6afcd2 100644 --- a/client/src/components/Toolbar/GraphTool/GraphTool.jsx +++ b/client/src/components/Toolbar/GraphTool/GraphTool.jsx @@ -33,12 +33,18 @@ Paste Subgraph export default function GraphTool(props) { + let text_color = props.selected ? 'text-red-400' : ''; + + if (props.is_auto) { + text_color = 'hover:text-purple-600 text-blue-600'; + } + return ( -
+
- {props.children} + {props.children}
); } \ No newline at end of file diff --git a/client/src/components/Toolbar/Toolbar.jsx b/client/src/components/Toolbar/Toolbar.jsx index cee8210..900ebb0 100644 --- a/client/src/components/Toolbar/Toolbar.jsx +++ b/client/src/components/Toolbar/Toolbar.jsx @@ -179,6 +179,7 @@ export default function Toolbar( props ) { props.graphTool === 'iteration' ? props.handleSetProofTool(null) : props.handleSetProofTool('iteration')} + is_auto={true} > Iteration @@ -189,6 +190,7 @@ export default function Toolbar( props ) { props.graphTool === 'deiteration' ? props.handleSetProofTool(null) : props.handleSetProofTool('deiteration')} + is_auto={true} > Deiteration diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index 92e197f..c9197fc 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -434,8 +434,6 @@ export default class ExistentialGraph { if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'paste_subgraph', this.graphController.graph.getCells()); } - this.graphTool = null; - this.onGraphToolUse && this.onGraphToolUse(); console.log('hypergraph', this.hypergraph) diff --git a/client/src/main.css b/client/src/main.css index 4d233e0..8a033d3 100644 --- a/client/src/main.css +++ b/client/src/main.css @@ -1184,6 +1184,16 @@ video { color: rgb(71 85 105 / var(--tw-text-opacity)); } +.text-fuchsia-400 { + --tw-text-opacity: 1; + color: rgb(232 121 249 / var(--tw-text-opacity)); +} + +.text-blue-600 { + --tw-text-opacity: 1; + color: rgb(37 99 235 / var(--tw-text-opacity)); +} + .underline { -webkit-text-decoration-line: underline; text-decoration-line: underline; @@ -1347,6 +1357,21 @@ html, body, #root, .app { color: rgb(71 85 105 / var(--tw-text-opacity)); } +.hover\:text-fuchsia-400:hover { + --tw-text-opacity: 1; + color: rgb(232 121 249 / var(--tw-text-opacity)); +} + +.hover\:text-purple-400:hover { + --tw-text-opacity: 1; + color: rgb(192 132 252 / var(--tw-text-opacity)); +} + +.hover\:text-purple-600:hover { + --tw-text-opacity: 1; + color: rgb(147 51 234 / var(--tw-text-opacity)); +} + .hover\:ring-1:hover { --tw-ring-offset-shadow: var(--tw-ring-inset) 0 0 0 var(--tw-ring-offset-width) var(--tw-ring-offset-color); --tw-ring-shadow: var(--tw-ring-inset) 0 0 0 calc(1px + var(--tw-ring-offset-width)) var(--tw-ring-color); diff --git a/client/src/views/Create/Create.jsx b/client/src/views/Create/Create.jsx index bcdb0f3..936121a 100644 --- a/client/src/views/Create/Create.jsx +++ b/client/src/views/Create/Create.jsx @@ -14,15 +14,24 @@ const GRAPH_STATE = { PROOF: 1 } +function useForceUpdate(){ + const [value, setValue] = useState(0); // integer state + return () => setValue(value => value + 1); // update state to force render + // A function that increment 👆🏻 the previous state like here + // is better than directly setting `setValue(value + 1)` +} + export default function Create(props) { + const forceUpdate = useForceUpdate(); + const { id } = useParams(); console.log('default name', getLocalGraphByID(id).name); const [graphName, setGraphName] = useState(getLocalGraphByID(id).name); const [existentialHypergraph, setExistentialHypergraph] = useState(new ExistentialHypergraph()); const [eg, setExistentialGraph] = useState(null); const [graphTool, setGraphTool] = useState(''); - const [inProof, setInProof] = useState(false) + const [inProof, setInProof] = useState(false); useEffect(() => { setExistentialGraph(new ExistentialGraph('main-paper', id, existentialHypergraph)); @@ -64,8 +73,17 @@ export default function Create(props) { setGraphTool(graphTool); eg.onGraphToolUse = () => { setGraphTool(null); + eg.graphTool = null; eg.isProofTool = false; } + + if (graphTool === 'iteration' || graphTool === 'deiteration') { + console.log('adding (de)iter step'); + existentialHypergraph.addStep(eg.graphController.graph_id, graphTool, eg.graphController.graph.getCells()); + console.log('existential hypergraph', existentialHypergraph); + eg.onGraphToolUse(); + forceUpdate(); + } } const handleSetProofTool = (graphTool) => { From fd5bcb5f046d1e04487cd1feaa95b0b902c14232 Mon Sep 17 00:00:00 2001 From: Eddie Krystowski Date: Tue, 28 Nov 2023 02:21:49 -0500 Subject: [PATCH 35/35] let users navigate proof steps, make insert wait for confirmation in proof mode Co-Authored-By: Joseph Krystowski <65693478+joekrystowski@users.noreply.github.com> --- .../components/Paper/ProofView/ProofStep.jsx | 5 +- .../components/Paper/ProofView/ProofView.jsx | 96 +++--- .../Toolbar/GraphTool/GraphTool.jsx | 17 +- client/src/components/Toolbar/Toolbar.jsx | 184 ++++++++---- .../src/existential-graph/ExistentialGraph.js | 16 +- .../ExistentialHypergraph.js | 30 +- .../ExistentialHypergraphNode.js | 15 +- .../src/existential-graph/GraphController.js | 10 +- client/src/main.css | 277 +++++++++--------- client/src/util/joint-util.js | 5 +- client/src/views/Create/Create.jsx | 65 +++- 11 files changed, 450 insertions(+), 270 deletions(-) diff --git a/client/src/components/Paper/ProofView/ProofStep.jsx b/client/src/components/Paper/ProofView/ProofStep.jsx index 7acd2d6..16c998d 100644 --- a/client/src/components/Paper/ProofView/ProofStep.jsx +++ b/client/src/components/Paper/ProofView/ProofStep.jsx @@ -13,7 +13,10 @@ const ruleMap = { export default function ProofStep(props) { return ( -
+
{ ruleMap[props.rule] || '???'}
) diff --git a/client/src/components/Paper/ProofView/ProofView.jsx b/client/src/components/Paper/ProofView/ProofView.jsx index 83560b8..dc22c91 100644 --- a/client/src/components/Paper/ProofView/ProofView.jsx +++ b/client/src/components/Paper/ProofView/ProofView.jsx @@ -11,52 +11,66 @@ export default function ProofView(props) { setExpanded(!expanded); } + return ( +
+
+ { + props.show && + + } + { + props.show && expanded && +
+ { + props.hypergraph.toArray().map((node, i) => ( + props.handleChangeHypergraphIndex(i)} + /> + )) - + // this.state.data.map((history_item, num) => ( + // (num === 0) ? null : + // + // )) + } +
+ } + +
- return ( -
- { - props.show && - - } - - { - props.show && expanded && -
- { - props.hypergraph.toArray().map((node, i) => ( - - )) - - // this.state.data.map((history_item, num) => ( - // (num === 0) ? null : - // - // )) +
+ { + props.show && +
+ +

Step {props.index + 1} / {props.hypergraph.toArray().length}

+ +
+ } +
- } -
+ ) } \ No newline at end of file diff --git a/client/src/components/Toolbar/GraphTool/GraphTool.jsx b/client/src/components/Toolbar/GraphTool/GraphTool.jsx index a6afcd2..b0a082f 100644 --- a/client/src/components/Toolbar/GraphTool/GraphTool.jsx +++ b/client/src/components/Toolbar/GraphTool/GraphTool.jsx @@ -19,7 +19,9 @@ const imageMap = { 'Copy Subgraph' : copySubgraphPng, 'Paste Subgraph' : pasteSubgraphPng, 'Iteration' : iterationPng, - 'Deiteration' : deiterationPng + 'Deiteration' : deiterationPng, + 'Confirm Insertion': insertSubgraphPng, + 'Cancel Insertion': removeSubgraphPng }; /** @@ -44,7 +46,18 @@ export default function GraphTool(props) { - {props.children} + + { props.requiresConfirmation + ? ( + props.waitingOnConfirmation + ?
+ + +
+ : props.children + ) + : props.children} +
); } \ No newline at end of file diff --git a/client/src/components/Toolbar/Toolbar.jsx b/client/src/components/Toolbar/Toolbar.jsx index 900ebb0..9fe3a52 100644 --- a/client/src/components/Toolbar/Toolbar.jsx +++ b/client/src/components/Toolbar/Toolbar.jsx @@ -1,4 +1,4 @@ -import React from 'react'; +import React, { useState } from 'react'; import "@root/main.css"; // Tawilwind stylesheet import ToolbarItem from './ToolbarItem/ToolbarItem'; import ToolbarItemOption from './ToolbarItemOption/ToolbarItemOption'; @@ -17,6 +17,15 @@ export default function Toolbar( props ) { props.handleStartProofClicked(); } + function handleConfirm() { + //props.handleSetProofTool('auto_disable_insert'); + } + + function handleCancel() { + //props.handleChangeHypergraphIndex(props.hypergraphIndex); + } + + //const [waitingForInsertConfirmation, setWaitingForInsertConfirmation] = useState(false); return ( @@ -57,50 +66,76 @@ export default function Toolbar( props ) { {/* Graph tools */}
- props.graphTool === 'cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('cut')} - > - Cut - - props.graphTool === 'insert_double_cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('insert_double_cut')} - > - Insert Double Cut - - props.graphTool === 'erase_double_cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('erase_double_cut')} - > - Erase Double Cut - - props.graphTool === 'insert_subgraph' - ? props.handleSetGraphTool('auto_disable_insert') - : props.handleSetGraphTool('insert_subgraph')} - > - Insert Subgraph - - props.graphTool === 'erase_subgraph' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('erase_subgraph')} - > - Erase Subgraph - - props.graphTool === 'copy_subgraph' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('copy_subgraph')} - > - Copy Subgraph - - props.graphTool === 'paste_subgraph' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('paste_subgraph')} - > - Paste Subgraph - + + { + true && + props.graphTool === 'cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('cut')} + > + Cut + + } + { + true && + props.graphTool === 'insert_double_cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('insert_double_cut')} + > + Insert Double Cut + + } + { + true && + props.graphTool === 'erase_double_cut' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('erase_double_cut')} + > + Erase Double Cut + + } + + { + !props.inProof && !props.waitingForInsertConfirmation && + props.graphTool === 'insert_subgraph' + ? props.handleSetGraphTool('auto_disable_insert') + : props.handleSetGraphTool('insert_subgraph')} + > + Insert Subgraph + + } + + { + !props.inProof && !props.waitingForInsertConfirmation && + props.graphTool === 'erase_subgraph' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('erase_subgraph')} + > + Erase Subgraph + + } + + { + true && + props.graphTool === 'copy_subgraph' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('copy_subgraph')} + > + Copy Subgraph + + } + + { + true && + props.graphTool === 'paste_subgraph' ? props.handleSetGraphTool(null) : props.handleSetGraphTool('paste_subgraph')} + > + Paste Subgraph + + } { props.inProof && @@ -132,7 +167,7 @@ export default function Toolbar( props ) { */} { - props.inProof && + props.inProof && !props.waitingForInsertConfirmation && props.graphTool === 'insert_double_cut' ? props.handleSetProofTool(null) : props.handleSetProofTool('insert_double_cut')} @@ -142,7 +177,7 @@ export default function Toolbar( props ) { } { - props.inProof && + props.inProof && !props.waitingForInsertConfirmation && props.graphTool === 'erase_double_cut' ? props.handleSetProofTool(null) : props.handleSetProofTool('erase_double_cut')} @@ -151,8 +186,36 @@ export default function Toolbar( props ) { } + {/* { + props.inProof && + { + if (props.graphTool !== 'insert_subgraph' && props.graphTool !== 'inserting_subgraph') { + props.handleSetProofTool('insert_subgraph'); + } + }} + > + Insert Subgraph + + } + { props.inProof && + props.graphTool === 'erase_subgraph' ? props.handleSetProofTool(null) : props.handleSetProofTool('erase_subgraph')} + > + Erase Subgraph + + } */} + +{ + props.inProof && !props.waitingForInsertConfirmation && props.graphTool === 'insert_subgraph' @@ -164,7 +227,7 @@ export default function Toolbar( props ) { } { - props.inProof && + props.inProof && !props.waitingForInsertConfirmation && props.graphTool === 'erase_subgraph' ? props.handleSetProofTool(null) : props.handleSetProofTool('erase_subgraph')} @@ -173,9 +236,8 @@ export default function Toolbar( props ) { } - { - props.inProof && + props.inProof && !props.waitingForInsertConfirmation && props.graphTool === 'iteration' ? props.handleSetProofTool(null) : props.handleSetProofTool('iteration')} @@ -186,7 +248,7 @@ export default function Toolbar( props ) { } { - props.inProof && + props.inProof && !props.waitingForInsertConfirmation && props.graphTool === 'deiteration' ? props.handleSetProofTool(null) : props.handleSetProofTool('deiteration')} @@ -195,6 +257,26 @@ export default function Toolbar( props ) { Deiteration } + + { + props.inProof && props.waitingForInsertConfirmation && + props.graphTool === 'confirm_insertion' ? props.handleSetProofTool(null) : props.handleSetProofTool('confirm_insertion')} + > + Confirm Insertion + + } + + { + props.inProof && props.waitingForInsertConfirmation && + props.graphTool === 'cancel_insertion' ? props.handleSetProofTool(null) : props.handleSetProofTool('cancel_insertion')} + > + Cancel Insertion + + }
diff --git a/client/src/existential-graph/ExistentialGraph.js b/client/src/existential-graph/ExistentialGraph.js index c9197fc..c6adfe3 100644 --- a/client/src/existential-graph/ExistentialGraph.js +++ b/client/src/existential-graph/ExistentialGraph.js @@ -287,7 +287,7 @@ export default class ExistentialGraph { for(let i = 0; i < graphJSON.cells.length; i++) { delete graphJSON.cells[i].graphController; } - + return graphJSON; } @@ -405,33 +405,33 @@ export default class ExistentialGraph { this.graphController.addCut(config); } - if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'cut', this.graphController.graph.getCells()); + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'cut', this.exportGraphAsJSON(), this.graphController.graph.getCells()); } else if (this.graphTool === 'insert_double_cut') { this.graphController.insertDoubleCut(this.selected_premise, this.getRelativeMousePos()) - if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'insert_double_cut', this.graphController.graph.getCells()); + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'insert_double_cut', this.exportGraphAsJSON(), this.graphController.graph.getCells()); } else if (this.graphTool === 'erase_double_cut') { if (!this.selected_premise) return; this.graphController.deleteDoubleCut(this.selected_premise); - if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'erase_double_cut', this.graphController.graph.getCells()); + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'erase_double_cut', this.exportGraphAsJSON(), this.graphController.graph.getCells()); } else if (this.graphTool === 'insert_subgraph') { console.log('test') this.graphController.enableInsertMode(this.selected_premise); - if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'insert_subgraph', this.graphController.graph.getCells()); + //if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'insert_subgraph', this.exportGraphAsJSON(), this.graphController.graph.getCells()); } else if (this.graphTool === 'erase_subgraph') { this.graphController.deleteSubgraph(this.selected_premise); - if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'erase_subgraph', this.graphController.graph.getCells()); + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'erase_subgraph', this.exportGraphAsJSON(), this.graphController.graph.getCells()); } else if (this.graphTool === 'copy_subgraph') { this.copySubgraph(this.selected_premise); - if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'copy_subgraph', this.graphController.graph.getCells()); + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'copy_subgraph', this.exportGraphAsJSON(), this.graphController.graph.getCells()); } else if (this.graphTool === 'paste_subgraph') { this.pasteSubgraph(this.selected_premise, this.getRelativeMousePos()); - if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'paste_subgraph', this.graphController.graph.getCells()); + if (this.proofMode && this.isProofTool) this.hypergraph.addStep(this.graphController.graph_id, 'paste_subgraph', this.exportGraphAsJSON(), this.graphController.graph.getCells()); } this.onGraphToolUse && this.onGraphToolUse(); diff --git a/client/src/existential-graph/ExistentialHypergraph.js b/client/src/existential-graph/ExistentialHypergraph.js index 04a4cf2..874ccb6 100644 --- a/client/src/existential-graph/ExistentialHypergraph.js +++ b/client/src/existential-graph/ExistentialHypergraph.js @@ -9,16 +9,17 @@ import ExistentialHypergraphNode from "./ExistentialHypergraphNode"; * We represent proofs using Existential Hypergraphs */ export default class ExistentialHypergraph { - constructor(rootGraph) + constructor(rootNode) { - this.root = new ExistentialHypergraphNode(rootGraph); + this.root = rootNode; this.ptr = this.root; } - addStep(graphId, rule, destination) { + addStep(graphId, rule, json, cells) { //const hypergraphNode = this.find(graphId); //if (hypergraphNode) { - this.ptr = this.ptr.addTransition(rule, destination); + + this.ptr = this.ptr.addTransition(rule, cells, json); ////} } @@ -27,7 +28,7 @@ export default class ExistentialHypergraph { let current = this.root; const result = [{rule: "Start", verified: true}]; - while (current.next.length) { + while (current && current.next.length) { result.push({ rule: current.next[0].rule, verified: current.next[0].verified @@ -43,6 +44,25 @@ export default class ExistentialHypergraph { } + + getHypergraphNode(index) { + let current = this.root; + + let ctr = 0; + + while (current) { + + if (ctr === index) return current; + current = (current.next.length) ? current.next[0].destination : null; + ctr++; + if (ctr > 100000) { + break; + } + } + + return null; + } + find(graphId) { let current = [this.root] while(current.length > 0) { diff --git a/client/src/existential-graph/ExistentialHypergraphNode.js b/client/src/existential-graph/ExistentialHypergraphNode.js index 0e2fd53..88b499f 100644 --- a/client/src/existential-graph/ExistentialHypergraphNode.js +++ b/client/src/existential-graph/ExistentialHypergraphNode.js @@ -1,8 +1,13 @@ + + export default class ExistentialHypergraphNode { - constructor(existentialGraph) { - this.existentialGraph = existentialGraph; + constructor(cells, json) { + this.cells = cells; + this.json = JSON.parse(JSON.stringify(json)); + + console.log('CREATED WITH JSON', this.json); this.parent = null; this.next = []; @@ -10,11 +15,11 @@ export default class ExistentialHypergraphNode { this.verified = false; } - addTransition(rule, destination) { - const destinationNode = new ExistentialHypergraphNode(destination); + addTransition(rule, cells, json) { + const destinationNode = new ExistentialHypergraphNode(cells, json); this.next.push({ rule, - destination: destinationNode + destination: destinationNode, }); return destinationNode; diff --git a/client/src/existential-graph/GraphController.js b/client/src/existential-graph/GraphController.js index b5bdce9..9bb43c2 100644 --- a/client/src/existential-graph/GraphController.js +++ b/client/src/existential-graph/GraphController.js @@ -769,11 +769,11 @@ export default class GraphController { selected_premise.embed(new_cuts[0]); this.colorByLevel(selected_premise) this.pack(selected_premise) - }// else - // { - // new_cuts[1].embed(selected_premise) - // this.pack(selected_premise) - // } + } else + { + new_cuts[1].embed(selected_premise) + this.pack(selected_premise) + } this.handleCollisions(new_cuts[0]) } diff --git a/client/src/main.css b/client/src/main.css index 8a033d3..8348757 100644 --- a/client/src/main.css +++ b/client/src/main.css @@ -557,6 +557,10 @@ video { --tw-backdrop-sepia: ; } +.fixed { + position: fixed; +} + .absolute { position: absolute; } @@ -565,12 +569,13 @@ video { position: relative; } -.right-0 { - right: 0px; +.inset-x-1\/2 { + left: 50%; + right: 50%; } -.top-0 { - top: 0px; +.right-0 { + right: 0px; } .right-10 { @@ -581,6 +586,10 @@ video { top: 2rem; } +.bottom-10 { + bottom: 2.5rem; +} + .z-10 { z-index: 10; } @@ -601,11 +610,6 @@ video { margin: auto; } -.mx-4 { - margin-left: 1rem; - margin-right: 1rem; -} - .mx-2 { margin-left: 0.5rem; margin-right: 0.5rem; @@ -631,8 +635,16 @@ video { margin-right: 1rem; } -.ml-4 { - margin-left: 1rem; +.mr-2 { + margin-right: 0.5rem; +} + +.mb-1 { + margin-bottom: 0.25rem; +} + +.mt-1 { + margin-top: 0.25rem; } .inline-block { @@ -673,36 +685,25 @@ video { height: 100%; } -.max-h-60 { - max-height: 15rem; -} - -.max-h-\[60\%\] { - max-height: 60%; -} - -.max-h-72 { - max-height: 18rem; -} - .max-h-96 { max-height: 24rem; } -.min-h-\[2rem\] { - min-height: 2rem; -} - -.min-h-\[20px\] { - min-height: 20px; +.min-h-full { + min-height: 100%; } .min-h-\[200px\] { min-height: 200px; } -.min-h-full { - min-height: 100%; +.min-h-\[2rem\] { + min-height: 2rem; +} + +.min-h-max { + min-height: -webkit-max-content; + min-height: max-content; } .w-screen { @@ -737,15 +738,15 @@ video { width: 8rem; } +.w-96 { + width: 24rem; +} + .w-max { width: -webkit-max-content; width: max-content; } -.w-96 { - width: 24rem; -} - .min-w-\[2rem\] { min-width: 2rem; } @@ -764,6 +765,12 @@ video { transform-origin: bottom left; } +.translate-x-\[-50\%\] { + --tw-translate-x: -50%; + -webkit-transform: translate(var(--tw-translate-x), var(--tw-translate-y)) rotate(var(--tw-rotate)) skewX(var(--tw-skew-x)) skewY(var(--tw-skew-y)) scaleX(var(--tw-scale-x)) scaleY(var(--tw-scale-y)); + transform: translate(var(--tw-translate-x), var(--tw-translate-y)) rotate(var(--tw-rotate)) skewX(var(--tw-skew-x)) skewY(var(--tw-skew-y)) scaleX(var(--tw-scale-x)) scaleY(var(--tw-scale-y)); +} + .scale-95 { --tw-scale-x: .95; --tw-scale-y: .95; @@ -799,10 +806,6 @@ video { flex-direction: column; } -.items-start { - align-items: flex-start; -} - .items-center { align-items: center; } @@ -834,10 +837,6 @@ video { border-color: rgb(243 244 246 / var(--tw-divide-opacity)); } -.self-end { - align-self: flex-end; -} - .self-center { align-self: center; } @@ -846,10 +845,6 @@ video { justify-self: center; } -.overflow-scroll { - overflow: scroll; -} - .overflow-y-scroll { overflow-y: scroll; } @@ -866,10 +861,18 @@ video { border-radius: 9999px; } +.rounded-xl { + border-radius: 0.75rem; +} + .border-2 { border-width: 2px; } +.border-l-2 { + border-left-width: 2px; +} + .border-b-2 { border-bottom-width: 2px; } @@ -878,14 +881,6 @@ video { border-top-width: 0px; } -.border-l-4 { - border-left-width: 4px; -} - -.border-l-2 { - border-left-width: 2px; -} - .border-solid { border-style: solid; } @@ -894,24 +889,19 @@ video { border-style: none; } -.border-black { - --tw-border-opacity: 1; - border-color: rgb(0 0 0 / var(--tw-border-opacity)); -} - -.border-indigo-600 { +.border-slate-500 { --tw-border-opacity: 1; - border-color: rgb(79 70 229 / var(--tw-border-opacity)); + border-color: rgb(100 116 139 / var(--tw-border-opacity)); } -.border-slate-600 { +.border-slate-700 { --tw-border-opacity: 1; - border-color: rgb(71 85 105 / var(--tw-border-opacity)); + border-color: rgb(51 65 85 / var(--tw-border-opacity)); } -.border-slate-300 { +.border-black { --tw-border-opacity: 1; - border-color: rgb(203 213 225 / var(--tw-border-opacity)); + border-color: rgb(0 0 0 / var(--tw-border-opacity)); } .border-slate-400 { @@ -919,14 +909,9 @@ video { border-color: rgb(148 163 184 / var(--tw-border-opacity)); } -.border-slate-500 { - --tw-border-opacity: 1; - border-color: rgb(100 116 139 / var(--tw-border-opacity)); -} - -.border-slate-700 { +.border-slate-600 { --tw-border-opacity: 1; - border-color: rgb(51 65 85 / var(--tw-border-opacity)); + border-color: rgb(71 85 105 / var(--tw-border-opacity)); } .bg-white { @@ -943,9 +928,9 @@ video { background-color: transparent; } -.bg-slate-400 { +.bg-slate-300 { --tw-bg-opacity: 1; - background-color: rgb(148 163 184 / var(--tw-bg-opacity)); + background-color: rgb(203 213 225 / var(--tw-bg-opacity)); } .bg-blue-500 { @@ -958,29 +943,34 @@ video { background-color: rgb(22 163 74 / var(--tw-bg-opacity)); } -.bg-slate-600 { +.bg-slate-400 { --tw-bg-opacity: 1; - background-color: rgb(71 85 105 / var(--tw-bg-opacity)); + background-color: rgb(148 163 184 / var(--tw-bg-opacity)); } -.bg-slate-300 { +.bg-slate-100 { --tw-bg-opacity: 1; - background-color: rgb(203 213 225 / var(--tw-bg-opacity)); + background-color: rgb(241 245 249 / var(--tw-bg-opacity)); } -.bg-slate-100 { +.bg-green-200 { --tw-bg-opacity: 1; - background-color: rgb(241 245 249 / var(--tw-bg-opacity)); + background-color: rgb(187 247 208 / var(--tw-bg-opacity)); } -.bg-slate-700 { +.bg-green-100 { --tw-bg-opacity: 1; - background-color: rgb(51 65 85 / var(--tw-bg-opacity)); + background-color: rgb(220 252 231 / var(--tw-bg-opacity)); } -.bg-slate-500 { +.bg-emerald-100 { --tw-bg-opacity: 1; - background-color: rgb(100 116 139 / var(--tw-bg-opacity)); + background-color: rgb(209 250 229 / var(--tw-bg-opacity)); +} + +.bg-red-100 { + --tw-bg-opacity: 1; + background-color: rgb(254 226 226 / var(--tw-bg-opacity)); } .p-5 { @@ -1019,9 +1009,9 @@ video { padding-right: 1.5rem; } -.px-1 { - padding-left: 0.25rem; - padding-right: 0.25rem; +.py-3 { + padding-top: 0.75rem; + padding-bottom: 0.75rem; } .px-3 { @@ -1029,9 +1019,19 @@ video { padding-right: 0.75rem; } -.py-3 { - padding-top: 0.75rem; - padding-bottom: 0.75rem; +.px-4 { + padding-left: 1rem; + padding-right: 1rem; +} + +.py-2 { + padding-top: 0.5rem; + padding-bottom: 0.5rem; +} + +.px-1 { + padding-left: 0.25rem; + padding-right: 0.25rem; } .pl-2 { @@ -1070,11 +1070,21 @@ video { font-family: ui-serif, Georgia, Cambria, "Times New Roman", Times, serif; } +.text-3xl { + font-size: 1.875rem; + line-height: 2.25rem; +} + .text-xl { font-size: 1.25rem; line-height: 1.75rem; } +.text-xs { + font-size: 0.75rem; + line-height: 1rem; +} + .text-2xl { font-size: 1.5rem; line-height: 2rem; @@ -1095,21 +1105,11 @@ video { line-height: 1.5rem; } -.text-3xl { - font-size: 1.875rem; - line-height: 2.25rem; -} - .text-lg { font-size: 1.125rem; line-height: 1.75rem; } -.text-xs { - font-size: 0.75rem; - line-height: 1rem; -} - .font-medium { font-weight: 500; } @@ -1118,14 +1118,14 @@ video { font-weight: 600; } -.font-light { - font-weight: 300; -} - .font-bold { font-weight: 700; } +.font-light { + font-weight: 300; +} + .uppercase { text-transform: uppercase; } @@ -1139,6 +1139,11 @@ video { color: rgb(0 0 0 / var(--tw-text-opacity)); } +.text-slate-700 { + --tw-text-opacity: 1; + color: rgb(51 65 85 / var(--tw-text-opacity)); +} + .text-white { --tw-text-opacity: 1; color: rgb(255 255 255 / var(--tw-text-opacity)); @@ -1159,39 +1164,34 @@ video { color: rgb(59 130 246 / var(--tw-text-opacity)); } -.text-red-400 { +.text-slate-600 { --tw-text-opacity: 1; - color: rgb(248 113 113 / var(--tw-text-opacity)); + color: rgb(71 85 105 / var(--tw-text-opacity)); } -.text-slate-700 { +.text-red-400 { --tw-text-opacity: 1; - color: rgb(51 65 85 / var(--tw-text-opacity)); + color: rgb(248 113 113 / var(--tw-text-opacity)); } -.text-slate-400 { +.text-blue-600 { --tw-text-opacity: 1; - color: rgb(148 163 184 / var(--tw-text-opacity)); + color: rgb(37 99 235 / var(--tw-text-opacity)); } -.text-slate-200 { +.text-green-600 { --tw-text-opacity: 1; - color: rgb(226 232 240 / var(--tw-text-opacity)); + color: rgb(22 163 74 / var(--tw-text-opacity)); } -.text-slate-600 { +.text-green-700 { --tw-text-opacity: 1; - color: rgb(71 85 105 / var(--tw-text-opacity)); + color: rgb(21 128 61 / var(--tw-text-opacity)); } -.text-fuchsia-400 { +.text-red-700 { --tw-text-opacity: 1; - color: rgb(232 121 249 / var(--tw-text-opacity)); -} - -.text-blue-600 { - --tw-text-opacity: 1; - color: rgb(37 99 235 / var(--tw-text-opacity)); + color: rgb(185 28 28 / var(--tw-text-opacity)); } .underline { @@ -1327,6 +1327,11 @@ html, body, #root, .app { cursor: pointer; } +.hover\:bg-slate-200:hover { + --tw-bg-opacity: 1; + background-color: rgb(226 232 240 / var(--tw-bg-opacity)); +} + .hover\:bg-slate-300:hover { --tw-bg-opacity: 1; background-color: rgb(203 213 225 / var(--tw-bg-opacity)); @@ -1337,19 +1342,14 @@ html, body, #root, .app { background-color: rgb(241 245 249 / var(--tw-bg-opacity)); } -.hover\:bg-slate-200:hover { +.hover\:bg-red-200:hover { --tw-bg-opacity: 1; - background-color: rgb(226 232 240 / var(--tw-bg-opacity)); + background-color: rgb(254 202 202 / var(--tw-bg-opacity)); } -.hover\:bg-slate-500:hover { +.hover\:bg-emerald-200:hover { --tw-bg-opacity: 1; - background-color: rgb(100 116 139 / var(--tw-bg-opacity)); -} - -.hover\:bg-slate-400:hover { - --tw-bg-opacity: 1; - background-color: rgb(148 163 184 / var(--tw-bg-opacity)); + background-color: rgb(167 243 208 / var(--tw-bg-opacity)); } .hover\:text-slate-600:hover { @@ -1357,16 +1357,6 @@ html, body, #root, .app { color: rgb(71 85 105 / var(--tw-text-opacity)); } -.hover\:text-fuchsia-400:hover { - --tw-text-opacity: 1; - color: rgb(232 121 249 / var(--tw-text-opacity)); -} - -.hover\:text-purple-400:hover { - --tw-text-opacity: 1; - color: rgb(192 132 252 / var(--tw-text-opacity)); -} - .hover\:text-purple-600:hover { --tw-text-opacity: 1; color: rgb(147 51 234 / var(--tw-text-opacity)); @@ -1425,11 +1415,6 @@ html, body, #root, .app { background-color: rgb(100 116 139 / var(--tw-bg-opacity)); } - .dark\:bg-slate-400 { - --tw-bg-opacity: 1; - background-color: rgb(148 163 184 / var(--tw-bg-opacity)); - } - .dark\:text-white { --tw-text-opacity: 1; color: rgb(255 255 255 / var(--tw-text-opacity)); diff --git a/client/src/util/joint-util.js b/client/src/util/joint-util.js index 0d629c0..0b478ec 100644 --- a/client/src/util/joint-util.js +++ b/client/src/util/joint-util.js @@ -10,7 +10,8 @@ const order = []; const ids = {}; console.log(cells) - while (cells.length > 0) { + while (cells && cells.length > 0) { + console.log('cells', cells); const cell = cells.shift(); const type = cell.type; @@ -31,6 +32,8 @@ ids[cell.id] = true; } } + + console.log('----------------- DONE ------------------------') return order; } diff --git a/client/src/views/Create/Create.jsx b/client/src/views/Create/Create.jsx index 936121a..b79c32f 100644 --- a/client/src/views/Create/Create.jsx +++ b/client/src/views/Create/Create.jsx @@ -6,8 +6,11 @@ import { CreatePaperComponent } from '@components/Paper'; import ExistentialGraph from '../../existential-graph/ExistentialGraph'; import ExistentialHypergraph from '../../existential-graph/ExistentialHypergraph'; +import { getSafeCellAddOrder } from "@util"; + import { addToLocalGraphData, getLocalGraphByID } from '../../util/util'; import ProofView from '../../components/Paper/ProofView/ProofView'; +import ExistentialHypergraphNode from '../../existential-graph/ExistentialHypergraphNode'; const GRAPH_STATE = { CREATE: 0, @@ -28,10 +31,12 @@ export default function Create(props) { const { id } = useParams(); console.log('default name', getLocalGraphByID(id).name); const [graphName, setGraphName] = useState(getLocalGraphByID(id).name); - const [existentialHypergraph, setExistentialHypergraph] = useState(new ExistentialHypergraph()); + const [existentialHypergraph, setExistentialHypergraph] = useState(new ExistentialHypergraph(null)); const [eg, setExistentialGraph] = useState(null); const [graphTool, setGraphTool] = useState(''); const [inProof, setInProof] = useState(false); + const [hypergraphIndex, setHypergraphIndex] = useState(0); + const [waitingForInsertConfirmation, setWaitingForInsertConfirmation] = useState(false); useEffect(() => { setExistentialGraph(new ExistentialGraph('main-paper', id, existentialHypergraph)); @@ -40,7 +45,7 @@ export default function Create(props) { useEffect(() => { if (inProof) { console.log('proof successfully started'); - setExistentialHypergraph(new ExistentialHypergraph(eg)); + setExistentialHypergraph(new ExistentialHypergraph(new ExistentialHypergraphNode(eg.graphController.graph.getCells(), eg.exportGraphAsJSON()))); } }, [inProof]); @@ -50,6 +55,24 @@ export default function Create(props) { if (eg) eg.hypergraph = existentialHypergraph; }, [existentialHypergraph]) + useEffect(() => { + console.log('hindex', hypergraphIndex) + console.log(existentialHypergraph.getHypergraphNode(hypergraphIndex)); + let node = existentialHypergraph.getHypergraphNode(hypergraphIndex); + if (node && eg) { + const graphJSON = node.json; + console.log('json', node.json); + const order = getSafeCellAddOrder(JSON.parse(JSON.stringify(graphJSON.cells))); + eg.graphController.graph.clear(); + eg.addCellsInOrder(order); + } + + }, [hypergraphIndex]) + + const handleChangeHypergraphIndex = (newIndex) => { + setHypergraphIndex(Math.max(0, Math.min(newIndex, existentialHypergraph.toArray().length-1))); + } + const handleSaveGraph = () => { console.log('CREATE VIEW SAVING GRAPH', graphName, id); const graphJSON = eg.exportGraphAsJSON(); @@ -65,13 +88,20 @@ export default function Create(props) { if (graphTool === 'auto_disable_insert') { graphTool = null; eg.graphController.disableInsertMode(); - eg.steps.push('disable_insert_mode'); } console.log('set graph tool:', graphTool); eg.graphTool = graphTool; eg.isProofTool = isProofTool; setGraphTool(graphTool); eg.onGraphToolUse = () => { + if (isProofTool && graphTool !== 'insert_subgraph' && graphTool !== 'confirm_insertion' && graphTool !== 'cancel_insertion') { + setHypergraphIndex(hypergraphIndex + 1); + } + + if (graphTool === 'insert_subgraph' && isProofTool && !waitingForInsertConfirmation) { + setWaitingForInsertConfirmation(true); + } + setGraphTool(null); eg.graphTool = null; eg.isProofTool = false; @@ -79,11 +109,28 @@ export default function Create(props) { if (graphTool === 'iteration' || graphTool === 'deiteration') { console.log('adding (de)iter step'); - existentialHypergraph.addStep(eg.graphController.graph_id, graphTool, eg.graphController.graph.getCells()); + existentialHypergraph.addStep(eg.graphController.graph_id, graphTool, eg.exportGraphAsJSON(), eg.graphController.graph.getCells()); console.log('existential hypergraph', existentialHypergraph); eg.onGraphToolUse(); forceUpdate(); } + + if (graphTool === 'confirm_insertion') { + console.log('confirming insertion'); + existentialHypergraph.addStep(eg.graphController.graph_id, 'insert_subgraph', eg.exportGraphAsJSON(), eg.graphController.graph.getCells()); + setWaitingForInsertConfirmation(false); + eg.graphController.disableInsertMode(); + eg.onGraphToolUse(); + forceUpdate(); + } + + if (graphTool === 'cancel_insertion') { + setHypergraphIndex(hypergraphIndex); + setWaitingForInsertConfirmation(false); + eg.graphController.disableInsertMode(); + eg.onGraphToolUse(); + forceUpdate(); + } } const handleSetProofTool = (graphTool) => { @@ -110,6 +157,9 @@ export default function Create(props) { handleSetGraphTool={handleSetGraphTool} handleSetProofTool={handleSetProofTool} handleStartProofClicked={handleStartProofClicked} + hypergraphIndex={hypergraphIndex} + handleChangeHypergraphIndex={handleChangeHypergraphIndex} + waitingForInsertConfirmation={waitingForInsertConfirmation} graphTool={graphTool} inProof={inProof} /> @@ -119,7 +169,12 @@ export default function Create(props) { dom_id="main-paper" graph_id={id} /> - +