Skip to content

Commit 33548d0

Browse files
committed
Make left bar proof list show the selected proof & clicking on a left bar proof selects the proof
1 parent e1064d7 commit 33548d0

2 files changed

Lines changed: 33 additions & 3 deletions

File tree

index.html

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -116,6 +116,9 @@
116116
border-bottom: 1px solid white;
117117
padding: 1em 0.2em 1em 0.2em;
118118
}
119+
#left-bar ol li span {
120+
cursor: pointer;
121+
}
119122
.selected {
120123
background: #0d6efd;
121124
}
@@ -135,8 +138,10 @@
135138
position: absolute;
136139
top: 0;
137140
left: 0;
138-
background: #ddd;
139-
border: 1px solid black;
141+
color: white;
142+
border-radius: 0.5rem;
143+
background: #212529;
144+
border: 1px solid #212529;
140145
padding: 0.5em;
141146
z-index: 20;
142147
visibility: hidden;

src/app.js

Lines changed: 26 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -182,8 +182,10 @@ const refreshList = () => {
182182
let ol = document.querySelector('#left-bar ol')
183183
ol.innerHTML = ''
184184
proofs.forEach((entry, i) => {
185-
ol.innerHTML += `<li value="${i}">
185+
ol.innerHTML += `<li value="${i}" class="${entry.selected ? 'selected' : ''}">
186+
<span onclick="javascript:selectProof(${i})">
186187
${entry.proof.conclusion.unicode()}
188+
</span>
187189
<br>
188190
<button onclick="javascript:giveLatex(${i})" class="latex">L<sup>a</sup>T<sub>e</sub>X</button>
189191
<button onclick="javascript:removeProof(${i})">✖ Delete</button>
@@ -208,6 +210,29 @@ const refreshAll = () => {
208210
redrawAll()
209211
}
210212

213+
const createSelection = opt => {
214+
let root = opt.selected[0].root
215+
let index = proofs.findIndex(entry => root == entry.proof)
216+
proofs[index].selected = true
217+
refreshList()
218+
}
219+
const removeSelection = (opt, shouldRefresh = true) => {
220+
for (var i = 0; i < proofs.length; i++) {
221+
proofs[i].selected = false
222+
}
223+
if (shouldRefresh) { refreshList() }
224+
}
225+
canvas.on("selection:created", createSelection)
226+
canvas.on("selection:cleared", removeSelection)
227+
canvas.on("selection:updated", opt => {
228+
removeSelection(opt, false)
229+
createSelection(opt)
230+
})
231+
const selectProof = i => {
232+
canvas.setActiveObject(canvas.item(i))
233+
canvas.renderAll()
234+
}
235+
211236
document.getElementById('addLKGoal').addEventListener('click', async () => {
212237
addProof(new LKIncomplete(await modalSequentPrompt('Enter an LK goal sequent:')))
213238
})

0 commit comments

Comments
 (0)