Enhance ProofModel by group expansion functionality.#431
Enhance ProofModel by group expansion functionality.#431axif0 wants to merge 16 commits intozxcalc:masterfrom
Conversation
|
Hello, thank you for the PR. Can you add the missing type annotations to pass the lint checks? Thanks, Lia |
|
Hi @lia-approves , I’ve added the missing type annotations and pushed the update. |
|
Hi @axif0 , thanks for the PR. When the grouped rewrites are expanded, the rewrites that were part of the group do not appear to be selectable. It looks like you only make a visual change of how the grouped rewrites are displayed. Can you make it such that the rewrites are clickable and when you click on a sub rewrite, you see the changes in the diagram according to the rewrite? |
…eps, displaying their graphs and highlighting them in the UI.
|
Thank you for your review. @RazinShaikh . Updated by individual sub-steps within grouped proof steps |
|
Thanks, the main functionality works now. Just a few things that need to be polished now:
group.mp4
rename.mp4
hover.mp4Once these things have been polished, I can review the code and then we can merge it |
|
Updated reviews accordingly, thanks for your in detailed suggetion @RazinShaikh .
|
|
Hi, this is starting to look quite complete.
|
|
Thanks for the suggetion @boldar99 . |
…write_data, and unfusion_rewrite modules
|
This is looking great! A couple of minor things:
Screen.Recording.2026-02-24.at.22.51.58.mov |
zxlive/rewrite_action.py
Outdated
| anim_before, anim_after = make_animation(self, panel, g, matches_list, rem_verts_list) | ||
| panel.undo_stack.push(cmd, anim_before=anim_before, anim_after=anim_after) | ||
|
|
||
| # TODO: Narrow down the type of the first return value. |
There was a problem hiding this comment.
This comment was not added by @axif0 . I am looking at the changes and it seems that when @axif0 merged the main branch to the current branch, some things were merged incorrectly. Because I deleted this block and code in #441 which fixes mypy and flake8 errors but it is being added back by this PR due to some original merge issues here.
RazinShaikh
left a comment
RazinShaikh
left a comment
There was a problem hiding this comment.
it looks like when you merged main to the current branch, several files (all changes other than proof.py) were merged incorrectly. Can you fix that? Also, can you make sure the checks pass?
zxlive/proof.py
Outdated
| def rowCount(self, parent: Union[QModelIndex, QPersistentModelIndex] = QModelIndex()) -> int: | ||
| """The number of rows""" | ||
| # This is a quirk of Qt list models: Since they are based on tree models, the | ||
| # user has to specify the index of the parent. In a list, we always expect the | ||
| # parent to be `None` or the empty `QModelIndex()` | ||
| if not index or not index.isValid(): | ||
| if not parent or not parent.isValid(): |
There was a problem hiding this comment.
Why did you change index to parent?
zxlive/proof.py
Outdated
| QPoint, QPointF, QRect, QRectF, QSize, Qt) | ||
| from PySide6.QtGui import QColor, QFont, QFontMetrics, QMouseEvent, QPainter, QPainterPath, QPen, QPolygonF | ||
| from PySide6.QtWidgets import (QAbstractItemView, QInputDialog, QLineEdit, QListView, QMenu, |
There was a problem hiding this comment.
some imports are unused
zxlive/proof.py
Outdated
| def _rename_sub_step_dialog(self, step_idx: int, sub_idx: int) -> None: | ||
| # Kept for compatibility if needed, but implementation redirects or is replaced. | ||
| # Ideally removed, but for this refactor we can just remove the old method body | ||
| pass |
There was a problem hiding this comment.
What is this? Is this some AI generated code leftover?
There was a problem hiding this comment.
This PR is unrelated to unfusion so it shouldn't change anything in this file.
There was a problem hiding this comment.
This PR is unrelated to this file so it shouldn't change anything here.
zxlive/rewrite_action.py
Outdated
| anim_before, anim_after = make_animation(self, panel, g, matches_list, rem_verts_list) | ||
| panel.undo_stack.push(cmd, anim_before=anim_before, anim_after=anim_after) | ||
|
|
||
| # TODO: Narrow down the type of the first return value. |
There was a problem hiding this comment.
This comment was not added by @axif0 . I am looking at the changes and it seems that when @axif0 merged the main branch to the current branch, some things were merged incorrectly. Because I deleted this block and code in #441 which fixes mypy and flake8 errors but it is being added back by this PR due to some original merge issues here.
There was a problem hiding this comment.
This PR is unrelated to this file so it shouldn't change anything here.
…grouped step headers and sub-steps, improving hover and selection highlighting.
|
@RazinShaikh Apologies for the merge issue on my side. |
There was a problem hiding this comment.
Pull request overview
This PR enhances the proof visualization feature by adding expandable/collapsible functionality for grouped proof steps. The implementation allows users to click a triangle icon to expand grouped steps and see individual sub-steps in a tree-like structure, addressing issue #292.
Changes:
- Added expandable group UI with triangle indicators and sub-step tree visualization in the delegate paint method
- Implemented mouse interaction handlers for expanding/collapsing groups, selecting sub-steps, and inline renaming of sub-steps
- Enhanced the ProofModel with sub-step renaming capabilities and synchronized name updates between group headers and sub-steps
Comments suppressed due to low confidence (6)
zxlive/proof.py:208
- The arrow symbol was changed from "🡒" to "\u2192" (→). While both are valid Unicode arrows, this change affects the display. Ensure that the new arrow character is properly rendered in all fonts and on all platforms that the application targets. The Unicode character U+2192 (→) is more commonly supported than U+1F852 (🡒), so this is likely an improvement, but verify visual consistency across different operating systems.
"Grouped Steps: " + " \u2192 ".join(self.steps[i].display_name for i in range(start_index, end_index + 1)),
zxlive/proof.py:954
- The sub-step circle colors are hard-coded (QColor(30, 100, 200) for selected and QColor(70, 130, 180) for default) and don't respect the dark mode setting. For consistency with the rest of the UI, these colors should either use display_setting.effective_colors or have different values for dark vs light mode. Compare with line 826 which uses display_setting.effective_colors["z_spider"] for the main circle.
if is_sub_selected:
painter.setBrush(QColor(30, 100, 200)) # brighter blue when selected
r = self.sub_circle_radius + 1
else:
painter.setBrush(QColor(70, 130, 180)) # default steel-blue
r = self.sub_circle_radius
zxlive/proof.py:549
- The lambda captures
step_idxandsub_idxfrom the enclosing scope, which creates a closure. In Python, lambdas in loops or conditional blocks can have unexpected behavior due to late binding. While this particular case should work because the lambda is created and stored in the action_function_map within the same scope, and is executed before the scope exits, it's still a potential source of bugs if the code is refactored. Consider using a default argument to capture the values explicitly:lambda si=step_idx, ssi=sub_idx: self._open_sub_step_editor(si, ssi)
action_function_map[rename_sub_action] = lambda: self._open_sub_step_editor(step_idx, sub_idx)
zxlive/proof.py:373
- There are two consecutive blank lines here. According to PEP 8, there should be at most one blank line between method definitions within a class. Consider removing one of these blank lines to maintain consistent style.
zxlive/proof.py:317 - When setting a new model, the active sub-step editor (if any) should be cleaned up. If an editor is currently open and a new model is set, the editor will become orphaned and may reference invalid indices. Consider adding cleanup for _active_sub_editor here, such as calling
deleteLater()on it if it exists and setting it to None.
def set_model(self, model: ProofModel) -> None:
self.setModel(model)
self.expanded_groups.clear()
self.selected_sub_step = None
# it looks like the selectionModel is linked to the model, so after updating the model we need to reconnect the selectionModel signals.
self.selectionModel().selectionChanged.connect(self.proof_step_selected)
self.setCurrentIndex(model.index(len(model.steps), 0))
zxlive/proof.py:330
- When collapsing a group, if there's an active sub-step editor open for one of its sub-steps, the editor should be closed and cleaned up. The current code clears the selected_sub_step state but doesn't handle the _active_sub_editor. This could leave an orphaned editor visible after the group is collapsed. Consider adding a check to close and delete the editor if it exists and belongs to this step_index.
def toggle_group_expansion(self, step_index: int) -> None:
"""Toggle the expanded/collapsed state of a grouped step."""
if step_index in self.expanded_groups:
self.expanded_groups.discard(step_index)
# Clear sub-step selection when collapsing
if self.selected_sub_step and self.selected_sub_step[0] == step_index:
self.selected_sub_step = None
else:
self.expanded_groups.add(step_index)
model_index = self.model().index(step_index + 1, 0)
self.model().dataChanged.emit(model_index, model_index, [])
self.doItemsLayout()
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
zxlive/proof.py
Outdated
| self.steps[step_index] = Rewrite(old_step.display_name, old_step.rule, old_step.graph, new_grouped) | ||
|
|
||
| # Rerender | ||
| modelIndex = self.createIndex(step_index, 0) |
There was a problem hiding this comment.
Same issue as line 182-183: this should be self.createIndex(step_index + 1, 0) to correctly emit the dataChanged signal for the right model row. The step_index parameter is a 0-based index into the steps array, but model rows are offset by 1.
| modelIndex = self.createIndex(step_index, 0) | |
| modelIndex = self.createIndex(step_index + 1, 0) |
zxlive/proof.py
Outdated
| modelIndex = self.createIndex(index, 0) | ||
| self.dataChanged.emit(modelIndex, modelIndex, []) |
There was a problem hiding this comment.
The modelIndex creation uses createIndex(index, 0) but the parameter index refers to the steps array index (0-based), while the model's row numbering is offset by 1 (row 0 is "START", row N corresponds to steps[N-1]). This emits a dataChanged signal for the wrong row. Based on the pattern seen in line 644 and the data() method at line 96, this should be self.createIndex(index + 1, 0) to correctly notify about the change in the view's row coordinate system.
|
@axif0 are the comments in copilot's review about the index correct? I am not quite sure. |
…ividual sub-steps within grouped proof steps.
|
Found a bug. like If you edit the position of an edge or node on a sub-step now, it should smoothly animate into place, save to the stack and leave your sub-panels completely intact!
ya, I think, any element at position i in self.steps corresponds to i + 1 in the view's model rows. they need to issue a dataChanged event for row index + 1 rather than index. |
|
I have made some minor edits to make the subtree look better. Can you please fix the following:
Screen.Recording.2026-02-26.at.18.17.28.mov |
|
Updated and use
|
|
Highlighting still seems to block the dots and lines inside the expanded view but not when outside. Could you fix that? |
…ighlights are rendered in the background.
Sorry I misinterpreted you earlier. @boldar99
|
|
Hello, Anything else I need to do on my side? |
|
Hi, I'm quite pleased with how it looks and thought this was effectively done, so I did some testing which unfortunately resulted in finding a bug. Rather, you should drop all the rewrites from the group after the step from which you did the new rewrite, as well as everything after the group. If the size of the group is 1 then ungroup this. And then add the new rewrites after outside of the group. Screen.Recording.2026-02-27.at.18.19.31.mov |
…runcation and ungrouping, with corresponding undo functionality.
|
So, I understand like -
|
zxlive/proof.py
Outdated
| if index.isValid() and index.row() > 0: | ||
| step_idx = index.row() - 1 | ||
| if step_idx < len(self.model().steps): | ||
| step = self.model().steps[step_idx] | ||
| if step.grouped_rewrites is not None: | ||
| if step_idx in self.expanded_groups: | ||
| rect = self.visualRect(index) | ||
| sub_idx = self._sub_step_hit_test( | ||
| step_idx, int(event.pos().y()), rect.y() | ||
| ) | ||
| if sub_idx >= 0: | ||
| new_step = step_idx |
There was a problem hiding this comment.
Is there no better way to do this than 5 nested if statements?
zxlive/proof.py
Outdated
| if index.isValid() and index.row() > 0: | ||
| step_idx = index.row() - 1 | ||
| if step_idx < len(self.model().steps): | ||
| step = self.model().steps[step_idx] | ||
| if step.grouped_rewrites is not None: | ||
| delegate = self.itemDelegate() | ||
| if isinstance(delegate, ProofStepItemDelegate): | ||
| rect = self.visualRect(index) | ||
| # Check if clicking on the triangle | ||
| if self._triangle_hit_test(step_idx, int(event.pos().x()), int(event.pos().y()), |
There was a problem hiding this comment.
Is there no better way to do this than 5 nested if statements?
…methods for improved readability.
|
Removed the 5-level deep nested if-statements and use helper method for better readability. @RazinShaikh |
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 2 out of 2 changed files in this pull request and generated no new comments.
Comments suppressed due to low confidence (6)
zxlive/commands.py:94
ProofModeCommandcallsProofStepView._navigate_to_sub_step, which is a private method (leading underscore) and couples command logic to view internals. Consider making this a public method (e.g.,navigate_to_sub_step) or exposing a small public API for selecting/navigating sub-steps so future refactors don’t break undo/redo behavior.
def undo(self) -> None:
if self.sub_step:
self.step_view.selectionModel().blockSignals(True)
self.step_view.setCurrentIndex(self.step_view.model().index(self.proof_step_index, 0, QModelIndex()))
self.step_view.selectionModel().blockSignals(False)
self.step_view._navigate_to_sub_step(self.sub_step[0], self.sub_step[1])
else:
self.step_view.move_to_step(self.proof_step_index)
self.command.undo()
if self.sub_step:
self.step_view.model().set_sub_graph(self.sub_step[0], self.sub_step[1], self.command.g)
else:
self.step_view.model().set_graph(self.proof_step_index, self.command.g)
def redo(self) -> None:
if self.sub_step:
self.step_view.selectionModel().blockSignals(True)
self.step_view.setCurrentIndex(self.step_view.model().index(self.proof_step_index, 0, QModelIndex()))
self.step_view.selectionModel().blockSignals(False)
self.step_view._navigate_to_sub_step(self.sub_step[0], self.sub_step[1])
else:
zxlive/commands.py:473
AddRewriteStepintroduces_old_group_tail, but it’s never read anywhere (undo uses_old_group_rewriteinstead). Leaving unused state like this makes the command harder to reason about and can drift from the actual behavior. Either remove_old_group_tailor use it to restore the truncated group in undo (if that was the intent).
# When rewriting from inside a grouped sub-step, stores the tail sub-steps
# that were dropped from the group (for undo restoration).
_old_group_tail: list[Rewrite] | None = field(default=None, init=False)
# The original Rewrite object for the group step (before truncation).
_old_group_rewrite: Rewrite | None = field(default=None, init=False)
zxlive/proof.py:840
is_lastis computed but no longer used inpaint(), which is easy to miss when maintaining the drawing logic. Consider removing it or reintroducing its usage (e.g., to stop the timeline line at the last item) to avoid dead code.
# ── Main timeline line ──────────────────────────────────────────
is_last = index.row() == index.model().rowCount() - 1
zxlive/proof.py:355
expanded_groupsstores 0-based indices intomodel.steps, but those indices will become stale when steps are inserted/removed (e.g., add/pop/group/ungroup), causing the wrong group to appear expanded or hit-testing/hover to mismatch. Consider tracking expansion byQPersistentModelIndex/stable IDs, or at least clearing/updatingexpanded_groups(andselected_sub_step) onrowsInserted/rowsRemoved/modelResetsignals.
self.expanded_groups: set[int] = set()
# Track currently selected sub-step: (step_index, sub_step_index) or None
self.selected_sub_step: tuple[int, int] | None = None
self._active_sub_editor: QLineEdit | None = None
self.setModel(ProofModel(self.graph_view.graph_scene.g))
self.setCurrentIndex(self.model().index(0, 0))
self.setEditTriggers(QAbstractItemView.EditTrigger.DoubleClicked)
# Set background color for dark mode (panel background)
if display_setting.dark_mode:
self.setStyleSheet("background-color: #23272e;")
else:
self.setStyleSheet("")
# Set background color for dark mode
pal = self.palette()
if display_setting.dark_mode:
pal.setColor(self.backgroundRole(), QColor(35, 39, 46))
pal.setColor(self.viewport().backgroundRole(), QColor(35, 39, 46))
else:
pal.setColor(self.backgroundRole(), QColor(255, 255, 255))
pal.setColor(self.viewport().backgroundRole(), QColor(255, 255, 255))
self.setPalette(pal)
self.setSpacing(0)
self.setMouseTracking(True)
self.setSelectionMode(QAbstractItemView.SelectionMode.ContiguousSelection)
self.setSelectionBehavior(QAbstractItemView.SelectionBehavior.SelectRows)
self.setResizeMode(QListView.ResizeMode.Adjust)
self.setUniformItemSizes(False)
self.setAlternatingRowColors(True)
self.viewport().setAttribute(Qt.WidgetAttribute.WA_Hover)
self.setContextMenuPolicy(Qt.ContextMenuPolicy.CustomContextMenu)
self.customContextMenuRequested.connect(self.show_context_menu)
self.selectionModel().selectionChanged.connect(self.proof_step_selected)
self.setItemDelegate(ProofStepItemDelegate(self))
# overriding this method to change the return type and stop mypy from complaining
def model(self) -> ProofModel:
model = super().model()
assert isinstance(model, ProofModel)
return model
def set_model(self, model: ProofModel) -> None:
self.setModel(model)
self.expanded_groups.clear()
self.selected_sub_step = None
# it looks like the selectionModel is linked to the model, so after updating the model we need to reconnect the selectionModel signals.
self.selectionModel().selectionChanged.connect(self.proof_step_selected)
self.setCurrentIndex(model.index(len(model.steps), 0))
def toggle_group_expansion(self, step_index: int) -> None:
"""Toggle the expanded/collapsed state of a grouped step."""
if step_index in self.expanded_groups:
self.expanded_groups.discard(step_index)
# Clear sub-step selection when collapsing
if self.selected_sub_step and self.selected_sub_step[0] == step_index:
self.selected_sub_step = None
else:
self.expanded_groups.add(step_index)
model_index = self.model().index(step_index + 1, 0)
self.model().dataChanged.emit(model_index, model_index, [])
self.doItemsLayout()
zxlive/proof.py:395
_sub_step_hit_test/_triangle_hit_testcomputerow_heightusingQFontMetrics(self.font()), but the delegate paints usingoption.font(and the model provides a per-itemFontRole). If the view font differs from the item font, hit-testing and hover/click detection will be misaligned. Use the same font metrics as painting (e.g., fetch the row font viaindex.data(Qt.FontRole)for the clicked row) when computingrow_height.
def _sub_step_hit_test(self, step_idx: int, event_pos_y: int, rect_y: int) -> int:
"""Determine which sub-step (if any) was clicked in an expanded group.
Returns the 0-based sub-step index, or -1 if the click was not on a sub-step.
"""
delegate = self.itemDelegate()
if not isinstance(delegate, ProofStepItemDelegate):
return -1
step = self.model().steps[step_idx]
if step.grouped_rewrites is None:
return -1
text_h = QFontMetrics(self.font()).height()
row_height = text_h + 2 * delegate.vert_padding
header_h = row_height # header occupies first row_height pixels
click_y = event_pos_y - rect_y
if click_y <= header_h:
return -1 # Click is in the header area
sub_y = click_y - header_h
sub_idx = int(sub_y // row_height)
if 0 <= sub_idx < len(step.grouped_rewrites):
return sub_idx
return -1
def _triangle_hit_test(self, step_idx: int, event_pos_x: int, event_pos_y: int, rect_x: int, rect_y: int) -> bool:
"""Check if the click was on the collapse/expand triangle."""
delegate = self.itemDelegate()
if not isinstance(delegate, ProofStepItemDelegate):
return False
text_h = QFontMetrics(self.font()).height()
row_height = text_h + 2 * delegate.vert_padding
text_x_base = rect_x + delegate.line_width + 2 * delegate.line_padding
tri_size = delegate.triangle_size
tri_cy = rect_y + row_height / 2
click_x = event_pos_x
click_y = event_pos_y
# Triangle bounds: roughly text_x_base to text_x_base + tri_size*2
# and tri_cy - tri_size to tri_cy + tri_size
return (text_x_base <= click_x <= text_x_base + tri_size * 2 and
tri_cy - tri_size <= click_y <= tri_cy + tri_size)
zxlive/proof.py:655
_open_sub_step_editorplaces theQLineEditusing coordinates fromvisualRect()(viewport coordinates), but creates the editor with parentself(theQListView). This can offset the editor when the view has a frame/scrolling because the coordinate systems differ. Prefer parenting the editor toself.viewport()(or mapping the rect to the view coordinate system) and includerect.x()in the x-position calculations so it stays aligned under horizontal scrolling/styling.
# Ensure the item is visible
model_idx = self.model().index(step_idx + 1, 0)
self.scrollTo(model_idx)
# Get the visual rect of the main item
rect = self.visualRect(model_idx)
# Calculate sub-step position logic (matching delegate.paint)
font = self.font()
text_height = QFontMetrics(font).height()
row_height = text_height + 2 * delegate.vert_padding
main_cx = delegate.line_padding + delegate.line_width / 2
sub_tree_x = main_cx + delegate.sub_indent
# Calculate vertical position of the sub-step
# Header + sub_steps before this one
header_height = row_height
sub_step_top = rect.y() + header_height + sub_idx * row_height
sub_text_x = int(sub_tree_x + delegate.circle_radius + 10)
editor_x = sub_text_x
# Center vertically in the row
editor_y = int(sub_step_top + delegate.vert_padding)
editor_w = rect.width() - sub_text_x - 5 # Small padding on right
editor_h = text_height
editor = QLineEdit(self)
step = self.model().steps[step_idx]
if step.grouped_rewrites:
editor.setText(step.grouped_rewrites[sub_idx].display_name)
editor.setGeometry(editor_x, editor_y, editor_w, editor_h)
# Style to blend in or look like an editor
if display_setting.dark_mode:
editor.setStyleSheet("QLineEdit { background-color: #2c313a; color: #e0e0e0; border: 1px solid #4b5362; }")
else:
editor.setStyleSheet("QLineEdit { background-color: white; color: black; border: 1px solid #ccc; }")
# Connect signals
editor.editingFinished.connect(lambda: self._finish_sub_step_edit(step_idx, sub_idx, editor))
editor.show()
editor.setFocus()
self._active_sub_editor = editor
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Enhance ProofStepView with expandable grouped steps and improve item rendering. Added functionality to toggle group expansion on mouse click and updated rendering logic in ProofStepItemDelegate for grouped steps.
Closed: #292