From d1f1b7374e3b4950034dd6c31186411c5a38d97a Mon Sep 17 00:00:00 2001 From: axif Date: Sun, 15 Feb 2026 04:49:53 +0600 Subject: [PATCH 01/19] Enhance ProofModel by group expansion functionality. --- zxlive/proof.py | 267 ++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 224 insertions(+), 43 deletions(-) diff --git a/zxlive/proof.py b/zxlive/proof.py index 146c56d2..a7f126e4 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -7,7 +7,7 @@ from PySide6.QtCore import (QAbstractItemModel, QAbstractListModel, QItemSelection, QModelIndex, QPersistentModelIndex, QPoint, QPointF, QRect, QSize, Qt) -from PySide6.QtGui import QColor, QFont, QFontMetrics, QPainter, QPen +from PySide6.QtGui import QColor, QFont, QFontMetrics, QPainter, QPen, QPolygonF from PySide6.QtWidgets import (QAbstractItemView, QLineEdit, QListView, QMenu, QStyle, QStyledItemDelegate, QStyleOptionViewItem, QWidget) @@ -114,12 +114,12 @@ def columnCount(self, index: Union[QModelIndex, QPersistentModelIndex] = QModelI """The number of columns""" return 1 - def rowCount(self, index: Union[QModelIndex, QPersistentModelIndex] = QModelIndex()) -> int: + 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(): return len(self.steps) + 1 else: return 0 @@ -169,7 +169,7 @@ def rename_step(self, index: int, name: str) -> None: def group_steps(self, start_index: int, end_index: int) -> None: """Replace the individual steps from `start_index` to `end_index` with a new grouped step""" new_rewrite = Rewrite( - "Grouped Steps: " + " 🡒 ".join(self.steps[i].display_name for i in range(start_index, end_index + 1)), + "Grouped Steps: " + " \u2192 ".join(self.steps[i].display_name for i in range(start_index, end_index + 1)), "Grouped", self.get_graph(end_index + 1), self.steps[start_index:end_index + 1] @@ -232,6 +232,7 @@ def __init__(self, parent: 'ProofPanel'): super().__init__(parent) self.graph_view = parent.graph_view self.undo_stack = parent.undo_stack + self.expanded_groups: set[int] = set() self.setModel(ProofModel(self.graph_view.graph_scene.g)) self.setCurrentIndex(self.model().index(0, 0)) self.setEditTriggers(QAbstractItemView.EditTrigger.DoubleClicked) @@ -253,7 +254,7 @@ def __init__(self, parent: 'ProofPanel'): self.setSelectionMode(QAbstractItemView.SelectionMode.ContiguousSelection) self.setSelectionBehavior(QAbstractItemView.SelectionBehavior.SelectRows) self.setResizeMode(QListView.ResizeMode.Adjust) - self.setUniformItemSizes(True) + self.setUniformItemSizes(False) self.setAlternatingRowColors(True) self.viewport().setAttribute(Qt.WidgetAttribute.WA_Hover) self.setContextMenuPolicy(Qt.ContextMenuPolicy.CustomContextMenu) @@ -269,10 +270,54 @@ def model(self) -> ProofModel: def set_model(self, model: ProofModel) -> None: self.setModel(model) + self.expanded_groups.clear() # 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) + 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() + + def mousePressEvent(self, event) -> None: # type: ignore[override] + """Handle mouse clicks on grouped steps to toggle expansion. + + Collapsed group: clicking anywhere on the row toggles expansion. + Expanded group: clicking in the header area (top row) collapses it; + clicking in the sub-step area only selects the step. + """ + index = self.indexAt(event.pos()) + toggle_idx = -1 + + 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): + if step_idx in self.expanded_groups: + # Expanded: only collapse when clicking the header row + rect = self.visualRect(index) + text_h = QFontMetrics(self.font()).height() + header_h = text_h + 2 * delegate.vert_padding + if event.pos().y() - rect.y() <= header_h: + toggle_idx = step_idx + else: + # Collapsed: any click on the row toggles + toggle_idx = step_idx + + super().mousePressEvent(event) + + if toggle_idx >= 0: + self.toggle_group_expansion(toggle_idx) + def move_to_step(self, index: int) -> None: idx = self.model().index(index, 0, QModelIndex()) self.clearSelection() @@ -357,6 +402,7 @@ class ProofStepItemDelegate(QStyledItemDelegate): """This class controls the painting of items in the proof steps list view. We paint a "git-style" line with circles to denote individual steps in a proof. + Grouped steps render as expandable tree nodes with sub-step branches. """ line_width = 3 @@ -367,9 +413,41 @@ class ProofStepItemDelegate(QStyledItemDelegate): circle_radius_selected = 6 circle_outline_width = 3 + # Sub-tree layout for expanded groups + triangle_size = 5 + sub_indent = 20 + sub_branch_len = 15 + sub_circle_radius = 3 + + def _step_info(self, index: Union[QModelIndex, QPersistentModelIndex]) -> tuple[bool, bool, Optional[list['Rewrite']]]: + """Return (is_grouped, is_expanded, grouped_rewrites) for a given row.""" + if index.row() == 0: + return False, False, None + model = index.model() + if not isinstance(model, ProofModel): + return False, False, None + step_idx = index.row() - 1 + if step_idx >= len(model.steps): + return False, False, None + step = model.steps[step_idx] + if step.grouped_rewrites is None: + return False, False, None + view = self.parent() + is_expanded = isinstance(view, ProofStepView) and step_idx in view.expanded_groups + return True, is_expanded, step.grouped_rewrites + def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> None: painter.save() - # Draw background + + is_grouped, is_expanded, grouped_rewrites = self._step_info(index) + + font = QFont(option.font) # type: ignore[attr-defined] + text_height = QFontMetrics(font).height() + row_height = text_height + 2 * self.vert_padding + fg = QColor(224, 224, 224) if display_setting.dark_mode else QColor(0, 0, 0) + line_clr = QColor(180, 180, 180) if display_setting.dark_mode else QColor(0, 0, 0) + + # ── Background ────────────────────────────────────────────────── painter.setPen(Qt.GlobalColor.transparent) if display_setting.dark_mode: if option.state & QStyle.StateFlag.State_Selected: # type: ignore[attr-defined] @@ -387,59 +465,162 @@ def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QM painter.setBrush(Qt.GlobalColor.white) painter.drawRect(option.rect) # type: ignore[attr-defined] - # Draw line + # ── Main timeline line ────────────────────────────────────────── is_last = index.row() == index.model().rowCount() - 1 + if is_last: + line_h = int(row_height / 2) + else: + line_h = int(option.rect.height()) # type: ignore[attr-defined] line_rect = QRect( self.line_padding, int(option.rect.y()), # type: ignore[attr-defined] self.line_width, - int(option.rect.height() if not is_last else option.rect.height() / 2) # type: ignore[attr-defined] + line_h ) - if display_setting.dark_mode: - painter.setBrush(QColor(180, 180, 180)) - else: - painter.setBrush(Qt.GlobalColor.black) + painter.setPen(Qt.GlobalColor.transparent) + painter.setBrush(line_clr) painter.drawRect(line_rect) - # Draw circle - if display_setting.dark_mode: - painter.setPen(QPen(QColor(180, 180, 180), self.circle_outline_width)) - else: - painter.setPen(QPen(Qt.GlobalColor.black, self.circle_outline_width)) + # ── Main circle ───────────────────────────────────────────────── + circle_cy = option.rect.y() + row_height / 2 # type: ignore[attr-defined] + painter.setPen(QPen(line_clr, self.circle_outline_width)) painter.setBrush(display_setting.effective_colors["z_spider"]) - circle_radius = self.circle_radius_selected if option.state & QStyle.StateFlag.State_Selected else self.circle_radius # type: ignore[attr-defined] - painter.drawEllipse( - QPointF(self.line_padding + self.line_width / 2, option.rect.y() + option.rect.height() / 2), # type: ignore[attr-defined] - circle_radius, - circle_radius + cr = self.circle_radius_selected \ + if option.state & QStyle.StateFlag.State_Selected else self.circle_radius # type: ignore[attr-defined] + main_cx = self.line_padding + self.line_width / 2 + painter.drawEllipse(QPointF(main_cx, circle_cy), cr, cr) + + # ── Text / group indicator ────────────────────────────────────── + text_x_base = int(option.rect.x() + self.line_width + 2 * self.line_padding) # type: ignore[attr-defined] + + if is_grouped: + s = self.triangle_size + tri_cy = int(option.rect.y() + row_height / 2) # type: ignore[attr-defined] + painter.setPen(Qt.GlobalColor.transparent) + painter.setBrush(fg) + + if is_expanded: + # Down-pointing triangle ▼ + triangle = QPolygonF([ + QPointF(text_x_base, tri_cy - s * 0.5), + QPointF(text_x_base + s * 2, tri_cy - s * 0.5), + QPointF(text_x_base + s, tri_cy + s * 0.5 + 1), + ]) + else: + # Right-pointing triangle ▶ + triangle = QPolygonF([ + QPointF(text_x_base, tri_cy - s), + QPointF(text_x_base + s, tri_cy), + QPointF(text_x_base, tri_cy + s), + ]) + painter.drawPolygon(triangle) + + tri_offset = s * 2 + 4 + header_text = "Grouped Steps" if is_expanded else index.data(Qt.ItemDataRole.DisplayRole) + text_rect = QRect( + text_x_base + tri_offset, + int(option.rect.y() + row_height / 2 - text_height / 2), # type: ignore[attr-defined] + int(option.rect.width() - self.line_width - 2 * self.line_padding - tri_offset), # type: ignore[attr-defined] + text_height + ) + bold_font = QFont(font) + bold_font.setWeight(QFont.Weight.Bold) + painter.setFont(bold_font) + painter.setPen(fg) + painter.drawText(text_rect, Qt.AlignmentFlag.AlignLeft, header_text) + + # Draw expanded sub-tree + if is_expanded and grouped_rewrites: + self._paint_sub_tree(painter, option, grouped_rewrites, + row_height, text_height, font, fg, line_clr) + else: + # Regular (non-grouped) step text + text = index.data(Qt.ItemDataRole.DisplayRole) + text_rect = QRect( + text_x_base, + int(option.rect.y() + row_height / 2 - text_height / 2), # type: ignore[attr-defined] + int(option.rect.width() - self.line_width - 2 * self.line_padding), # type: ignore[attr-defined] + text_height + ) + draw_font = QFont(font) + if option.state & QStyle.StateFlag.State_Selected: # type: ignore[attr-defined] + draw_font.setWeight(QFont.Weight.Bold) + painter.setFont(draw_font) + painter.setPen(fg) + painter.drawText(text_rect, Qt.AlignmentFlag.AlignLeft, text) + + painter.restore() + + # ── Expanded sub-tree painting ────────────────────────────────────── + def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, + grouped_rewrites: list['Rewrite'], row_height: int, + text_height: int, font: QFont, + fg: QColor, line_clr: QColor) -> None: + main_cx = self.line_padding + self.line_width / 2 + sub_tree_x = main_cx + self.sub_indent + n = len(grouped_rewrites) + + first_sub_top = option.rect.y() + row_height # type: ignore[attr-defined] + last_sub_cy = first_sub_top + (n - 1) * row_height + row_height / 2 + + pen = QPen(line_clr, 2) + painter.setPen(pen) + + # Diagonal connector from main circle down to start of sub-tree + header_cy = option.rect.y() + row_height / 2 # type: ignore[attr-defined] + painter.drawLine( + QPointF(main_cx, header_cy + self.circle_radius_selected), + QPointF(sub_tree_x, first_sub_top) ) - # Draw text - text = index.data(Qt.ItemDataRole.DisplayRole) - text_height = QFontMetrics(option.font).height() # type: ignore[attr-defined] - text_rect = QRect( - int(option.rect.x() + self.line_width + 2 * self.line_padding), # type: ignore[attr-defined] - int(option.rect.y() + option.rect.height() / 2 - text_height / 2), # type: ignore[attr-defined] - option.rect.width(), # type: ignore[attr-defined] - text_height + # Sub-tree vertical line + painter.drawLine( + QPointF(sub_tree_x, first_sub_top), + QPointF(sub_tree_x, last_sub_cy) ) - font = option.font # type: ignore[attr-defined] - if option.state & QStyle.StateFlag.State_Selected: # type: ignore[attr-defined] - font.setWeight(QFont.Weight.Bold) - painter.setFont(font) - if display_setting.dark_mode: - painter.setPen(QColor(224, 224, 224)) - painter.setBrush(QColor(224, 224, 224)) - else: - painter.setPen(Qt.GlobalColor.black) - painter.setBrush(Qt.GlobalColor.black) - painter.drawText(text_rect, Qt.AlignmentFlag.AlignLeft, text) - painter.restore() + sub_circle_cx = sub_tree_x + self.sub_branch_len + for i, sub_step in enumerate(grouped_rewrites): + sub_cy = first_sub_top + i * row_height + row_height / 2 + + # Horizontal branch + painter.setPen(pen) + painter.drawLine( + QPointF(sub_tree_x, sub_cy), + QPointF(sub_circle_cx - self.sub_circle_radius, sub_cy) + ) + + # Sub-step circle (steel-blue fill) + painter.setPen(QPen(line_clr, 2)) + painter.setBrush(QColor(70, 130, 180)) + painter.drawEllipse( + QPointF(sub_circle_cx, sub_cy), + self.sub_circle_radius, self.sub_circle_radius + ) + + # Sub-step text + sub_text_x = int(sub_circle_cx + self.sub_circle_radius + 8) + sub_text_rect = QRect( + sub_text_x, + int(sub_cy - text_height / 2), + int(option.rect.width() - sub_text_x), # type: ignore[attr-defined] + text_height + ) + painter.setFont(font) + painter.setPen(fg) + painter.drawText(sub_text_rect, Qt.AlignmentFlag.AlignLeft, sub_step.display_name) def sizeHint(self, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> QSize: size = super().sizeHint(option, index) - return QSize(size.width(), size.height() + 2 * self.vert_padding) + text_height = QFontMetrics(option.font).height() # type: ignore[attr-defined] + single_row = text_height + 2 * self.vert_padding + total = single_row + + is_grouped, is_expanded, grouped_rewrites = self._step_info(index) + if is_grouped and is_expanded and grouped_rewrites: + total += len(grouped_rewrites) * single_row + + return QSize(size.width(), total) def createEditor(self, parent: QWidget, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> QLineEdit: return QLineEdit(parent) From 1d5f5b288a5922ceac8b51813923b1fdde707732 Mon Sep 17 00:00:00 2001 From: axif Date: Tue, 17 Feb 2026 01:16:08 +0600 Subject: [PATCH 02/19] Fix mypy type errors and enhance type hints in proof and rewrite modules. --- zxlive/proof.py | 4 ++-- zxlive/rewrite_action.py | 12 ++++++------ zxlive/rewrite_data.py | 2 +- zxlive/unfusion_rewrite.py | 4 ++-- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/zxlive/proof.py b/zxlive/proof.py index a7f126e4..2cbf5954 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -7,7 +7,7 @@ from PySide6.QtCore import (QAbstractItemModel, QAbstractListModel, QItemSelection, QModelIndex, QPersistentModelIndex, QPoint, QPointF, QRect, QSize, Qt) -from PySide6.QtGui import QColor, QFont, QFontMetrics, QPainter, QPen, QPolygonF +from PySide6.QtGui import QColor, QFont, QFontMetrics, QMouseEvent, QPainter, QPen, QPolygonF from PySide6.QtWidgets import (QAbstractItemView, QLineEdit, QListView, QMenu, QStyle, QStyledItemDelegate, QStyleOptionViewItem, QWidget) @@ -285,7 +285,7 @@ def toggle_group_expansion(self, step_index: int) -> None: self.model().dataChanged.emit(model_index, model_index, []) self.doItemsLayout() - def mousePressEvent(self, event) -> None: # type: ignore[override] + def mousePressEvent(self, event: QMouseEvent) -> None: # type: ignore[override] """Handle mouse clicks on grouped steps to toggle expansion. Collapsed group: clicking anywhere on the row toggles expansion. diff --git a/zxlive/rewrite_action.py b/zxlive/rewrite_action.py index aa7577b2..cfed04ee 100644 --- a/zxlive/rewrite_action.py +++ b/zxlive/rewrite_action.py @@ -103,7 +103,7 @@ def do_rewrite(self, panel: ProofPanel) -> None: elif self.match_type == MATCH_SINGLE: matches = [v for v in verts if self.rule.is_match(g, v)] # type: ignore elif self.match_type == MATCH_DOUBLE: - matches = [g.edge_st(e) for e in edges if g.edge_st(e)[0] != g.edge_st(e)[1] and self.rule.is_match(g, *g.edge_st(e))] + matches = [g.edge_st(e) for e in edges if g.edge_st(e)[0] != g.edge_st(e)[1] and self.rule.is_match(g, *g.edge_st(e))] # type: ignore[attr-defined] elif self.match_type == MATCH_COMPOUND: # We don't necessarily have a matcher in this case # if self.rule.is_match(g, verts): if len(verts) == 0: @@ -118,9 +118,9 @@ def do_rewrite(self, panel: ProofPanel) -> None: for m in matches: if self.match_type == MATCH_DOUBLE: v1, v2 = cast(tuple[VT, VT], m) - if self.rule.apply(g, v1, v2): + if self.rule.apply(g, v1, v2): # type: ignore[attr-defined] applied = True - elif self.rule.apply(g, m): + elif self.rule.apply(g, m): # type: ignore[attr-defined] applied = True # g, rem_verts = self.apply_rewrite(g, matches) # rem_verts_list.extend(rem_verts) @@ -137,15 +137,15 @@ def do_rewrite(self, panel: ProofPanel) -> None: # TODO: Narrow down the type of the first return value. def apply_rewrite(self, g: GraphT, matches: list) -> tuple[GraphT, list[VT]]: if self.returns_new_graph: - graph = self.rule(g, matches) + graph = self.rule(g, matches) # type: ignore[call-arg] assert isinstance(graph, GraphT) return graph, [] for m in matches: if self.match_type == MATCH_DOUBLE: v1, v2 = cast(tuple[VT, VT], m) - self.rule.apply(g, v1, v2) - else: self.rule.apply(g, m) + self.rule.apply(g, v1, v2) # type: ignore[attr-defined] + else: self.rule.apply(g, m) # type: ignore[attr-defined] # rewrite = self.rule(g, matches) # assert isinstance(rewrite, tuple) and len(rewrite) == 4 # etab, rem_verts, rem_edges, check_isolated_vertices = rewrite diff --git a/zxlive/rewrite_data.py b/zxlive/rewrite_data.py index a4e16f97..7beb0d6a 100644 --- a/zxlive/rewrite_data.py +++ b/zxlive/rewrite_data.py @@ -133,7 +133,7 @@ def rule(g: GraphT, matches: list) -> bool: simplified = cast(GraphT, subgraph.copy()) strategy(simplified) return CustomRule(subgraph, simplified, "", "").applier(g, matches) - return RewriteSimpGraph(rule, rule) + return RewriteSimpGraph(rule, rule) # type: ignore[arg-type] def create_subgraph_with_boundary(graph: GraphT, verts: list[VT]) -> GraphT: verts = [v for v in verts if graph.type(v) != VertexType.BOUNDARY] diff --git a/zxlive/unfusion_rewrite.py b/zxlive/unfusion_rewrite.py index b9a487c4..c2bbabd7 100644 --- a/zxlive/unfusion_rewrite.py +++ b/zxlive/unfusion_rewrite.py @@ -44,7 +44,7 @@ def unfuse_rule_simp_applier(graph: BaseGraph[VT, ET]) -> bool: return True unfusion_rewrite: RewriteSimpGraph[VT, ET] = RewriteSimpGraph(apply_unfuse_rule, unfuse_rule_simp_applier) -unfusion_rewrite.is_match = match_unfuse_single_vertex +unfusion_rewrite.is_match = match_unfuse_single_vertex # type: ignore[attr-defined] class UnfusionRewriteAction: """Special rewrite action that handles the interactive unfusion process.""" @@ -166,7 +166,7 @@ def reassign_edges(edges: list[ET], node: VT) -> None: from .rewrite_data import rules_basic cmd = AddRewriteStep(self.proof_panel.graph_view, new_g, - self.proof_panel.step_view, rules_basic['unfuse']['text']) + self.proof_panel.step_view, str(rules_basic['unfuse']['text'])) anim = anims.unfuse(graph, new_g, original_vertex, self.proof_panel.graph_scene) self.proof_panel.undo_stack.push(cmd, anim_after=anim) From 3323321f005e7b14990d03860d4ec1841bee33ed Mon Sep 17 00:00:00 2001 From: axif Date: Tue, 17 Feb 2026 14:39:31 +0600 Subject: [PATCH 03/19] feat: Allow selection of individual sub-steps within grouped proof steps, displaying their graphs and highlighting them in the UI. --- zxlive/proof.py | 117 +++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 106 insertions(+), 11 deletions(-) diff --git a/zxlive/proof.py b/zxlive/proof.py index 2cbf5954..40105041 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -233,6 +233,8 @@ def __init__(self, parent: 'ProofPanel'): self.graph_view = parent.graph_view self.undo_stack = parent.undo_stack self.expanded_groups: set[int] = set() + # Track currently selected sub-step: (step_index, sub_step_index) or None + self.selected_sub_step: Optional[tuple[int, int]] = None self.setModel(ProofModel(self.graph_view.graph_scene.g)) self.setCurrentIndex(self.model().index(0, 0)) self.setEditTriggers(QAbstractItemView.EditTrigger.DoubleClicked) @@ -271,6 +273,7 @@ def model(self) -> ProofModel: 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)) @@ -279,21 +282,61 @@ 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() + 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 _navigate_to_sub_step(self, step_idx: int, sub_idx: int) -> None: + """Display the graph corresponding to a sub-step within a grouped rewrite.""" + step = self.model().steps[step_idx] + if step.grouped_rewrites is None or sub_idx < 0 or sub_idx >= len(step.grouped_rewrites): + return + self.selected_sub_step = (step_idx, sub_idx) + sub_graph = step.grouped_rewrites[sub_idx].graph.copy() + assert isinstance(sub_graph, GraphT) + self.graph_view.set_graph(sub_graph) + # Trigger repaint so the delegate can highlight the selected sub-step + model_index = self.model().index(step_idx + 1, 0) + self.model().dataChanged.emit(model_index, model_index, []) + def mousePressEvent(self, event: QMouseEvent) -> None: # type: ignore[override] """Handle mouse clicks on grouped steps to toggle expansion. Collapsed group: clicking anywhere on the row toggles expansion. Expanded group: clicking in the header area (top row) collapses it; - clicking in the sub-step area only selects the step. + clicking on a sub-step navigates to that sub-step's graph. """ index = self.indexAt(event.pos()) toggle_idx = -1 + sub_step_clicked = False if index.isValid() and index.row() > 0: step_idx = index.row() - 1 @@ -303,16 +346,29 @@ def mousePressEvent(self, event: QMouseEvent) -> None: # type: ignore[override] delegate = self.itemDelegate() if isinstance(delegate, ProofStepItemDelegate): if step_idx in self.expanded_groups: - # Expanded: only collapse when clicking the header row + # Expanded: check if clicking header or sub-step rect = self.visualRect(index) - text_h = QFontMetrics(self.font()).height() - header_h = text_h + 2 * delegate.vert_padding - if event.pos().y() - rect.y() <= header_h: + sub_idx = self._sub_step_hit_test( + step_idx, int(event.pos().y()), rect.y() + ) + if sub_idx >= 0: + # Clicked on a sub-step + sub_step_clicked = True + self._navigate_to_sub_step(step_idx, sub_idx) + else: + # Clicked on the header -> collapse toggle_idx = step_idx else: # Collapsed: any click on the row toggles toggle_idx = step_idx + # Clear sub-step selection when clicking on a non-sub-step area + if not sub_step_clicked and self.selected_sub_step is not None: + old_step_idx = self.selected_sub_step[0] + self.selected_sub_step = None + old_model_idx = self.model().index(old_step_idx + 1, 0) + self.model().dataChanged.emit(old_model_idx, old_model_idx, []) + super().mousePressEvent(event) if toggle_idx >= 0: @@ -361,6 +417,12 @@ def rename_proof_step(self, new_name: str, index: int) -> None: def proof_step_selected(self, selected: QItemSelection, deselected: QItemSelection) -> None: if not selected or not deselected: return + # Clear sub-step selection when a different main step is selected + if self.selected_sub_step is not None: + old_step_idx = self.selected_sub_step[0] + self.selected_sub_step = None + old_model_idx = self.model().index(old_step_idx + 1, 0) + self.model().dataChanged.emit(old_model_idx, old_model_idx, []) step_index = selected.first().topLeft().row() self.move_to_step(step_index) @@ -531,7 +593,8 @@ def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QM # Draw expanded sub-tree if is_expanded and grouped_rewrites: - self._paint_sub_tree(painter, option, grouped_rewrites, + self._paint_sub_tree(painter, option, index.row() - 1, + grouped_rewrites, row_height, text_height, font, fg, line_clr) else: # Regular (non-grouped) step text @@ -553,6 +616,7 @@ def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QM # ── Expanded sub-tree painting ────────────────────────────────────── def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, + step_idx: int, grouped_rewrites: list['Rewrite'], row_height: int, text_height: int, font: QFont, fg: QColor, line_clr: QColor) -> None: @@ -579,9 +643,33 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, QPointF(sub_tree_x, last_sub_cy) ) + # Determine which sub-step is selected (if any) + view = self.parent() + selected_sub_idx = -1 + if isinstance(view, ProofStepView) and view.selected_sub_step is not None: + sel_step_idx, sel_sub_idx = view.selected_sub_step + if step_idx == sel_step_idx: + selected_sub_idx = sel_sub_idx + sub_circle_cx = sub_tree_x + self.sub_branch_len for i, sub_step in enumerate(grouped_rewrites): sub_cy = first_sub_top + i * row_height + row_height / 2 + is_sub_selected = (i == selected_sub_idx) + + # Draw highlight background for selected sub-step + if is_sub_selected: + painter.setPen(Qt.GlobalColor.transparent) + if display_setting.dark_mode: + painter.setBrush(QColor(50, 90, 140, 120)) + else: + painter.setBrush(QColor(180, 215, 255, 160)) + highlight_rect = QRect( + int(sub_tree_x - 4), + int(sub_cy - row_height / 2), + int(option.rect.width() - sub_tree_x + 4), # type: ignore[attr-defined] + row_height + ) + painter.drawRect(highlight_rect) # Horizontal branch painter.setPen(pen) @@ -590,12 +678,16 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, QPointF(sub_circle_cx - self.sub_circle_radius, sub_cy) ) - # Sub-step circle (steel-blue fill) + # Sub-step circle painter.setPen(QPen(line_clr, 2)) - painter.setBrush(QColor(70, 130, 180)) + 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 painter.drawEllipse( - QPointF(sub_circle_cx, sub_cy), - self.sub_circle_radius, self.sub_circle_radius + QPointF(sub_circle_cx, sub_cy), r, r ) # Sub-step text @@ -606,7 +698,10 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, int(option.rect.width() - sub_text_x), # type: ignore[attr-defined] text_height ) - painter.setFont(font) + sub_font = QFont(font) + if is_sub_selected: + sub_font.setWeight(QFont.Weight.Bold) + painter.setFont(sub_font) painter.setPen(fg) painter.drawText(sub_text_rect, Qt.AlignmentFlag.AlignLeft, sub_step.display_name) From 0665d4ae3fb5d09af7141244bd1425ab7ed8d303 Mon Sep 17 00:00:00 2001 From: axif Date: Wed, 18 Feb 2026 23:09:50 +0600 Subject: [PATCH 04/19] Implement sub-step renaming with an inline editor --- zxlive/proof.py | 230 ++++++++++++++++++++++++++++++++++++------------ 1 file changed, 176 insertions(+), 54 deletions(-) diff --git a/zxlive/proof.py b/zxlive/proof.py index 38c5783d..2c91c55c 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -6,9 +6,9 @@ from PySide6.QtCore import (QAbstractItemModel, QAbstractListModel, QItemSelection, QModelIndex, QPersistentModelIndex, - QPoint, QPointF, QRect, QSize, Qt) -from PySide6.QtGui import QColor, QFont, QFontMetrics, QMouseEvent, QPainter, QPen, QPolygonF -from PySide6.QtWidgets import (QAbstractItemView, QLineEdit, QListView, QMenu, + 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, QStyle, QStyledItemDelegate, QStyleOptionViewItem, QWidget) @@ -182,6 +182,26 @@ def rename_step(self, index: int, name: str) -> None: modelIndex = self.createIndex(index, 0) self.dataChanged.emit(modelIndex, modelIndex, []) + def rename_sub_step(self, step_index: int, sub_index: int, name: str) -> None: + """Change the display name of a sub-step""" + old_step = self.steps[step_index] + grouped = old_step.grouped_rewrites + if grouped is None or sub_index >= len(grouped): + return + + old_sub_step = grouped[sub_index] + new_sub_step = Rewrite(name, old_sub_step.rule, old_sub_step.graph, old_sub_step.grouped_rewrites) + + new_grouped = list(grouped) + new_grouped[sub_index] = new_sub_step + + # Update the main step's grouped rewrites + self.steps[step_index] = Rewrite(old_step.display_name, old_step.rule, old_step.graph, new_grouped) + + # Rerender + modelIndex = self.createIndex(step_index, 0) + self.dataChanged.emit(modelIndex, modelIndex, []) + def group_steps(self, start_index: int, end_index: int) -> None: """Replace the individual steps from `start_index` to `end_index` with a new grouped step""" new_rewrite = Rewrite( @@ -251,6 +271,7 @@ def __init__(self, parent: 'ProofPanel'): self.expanded_groups: set[int] = set() # Track currently selected sub-step: (step_index, sub_step_index) or None self.selected_sub_step: Optional[tuple[int, int]] = None + self._active_sub_editor: Optional[QLineEdit] = None self.setModel(ProofModel(self.graph_view.graph_scene.g)) self.setCurrentIndex(self.model().index(0, 0)) self.setEditTriggers(QAbstractItemView.EditTrigger.DoubleClicked) @@ -499,11 +520,106 @@ def show_context_menu(self, position: QPoint) -> None: if self.model().steps[index - 1].grouped_rewrites is not None: ungroup_action = context_menu.addAction("Ungroup Steps") action_function_map[ungroup_action] = self.ungroup_selected_step + + # Check if we clicked on a sub-step + step_idx = index - 1 + if step_idx in self.expanded_groups: + rect = self.visualRect(selected_indexes[0]) + # We need the relative position within the item rect + # mapToGlobal(position) is global, position is local to widget + # position is passed from customContextMenuRequested, which is in widget coords + sub_idx = self._sub_step_hit_test( + step_idx, int(position.y()), rect.y() + ) + if sub_idx >= 0: + # If a sub-step is clicked, we probably want to rename the sub-step, + # not the parent group step. + context_menu.removeAction(rename_action) + rename_sub_action = context_menu.addAction("Rename Sub-step") + action_function_map[rename_sub_action] = lambda: self._open_sub_step_editor(step_idx, sub_idx) action = context_menu.exec_(self.mapToGlobal(position)) if action in action_function_map: action_function_map[action]() + def _open_sub_step_editor(self, step_idx: int, sub_idx: int) -> None: + """Opens an inline editor for renaming a sub-step.""" + delegate = self.itemDelegate() + if not isinstance(delegate, ProofStepItemDelegate): + return + + # 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.sub_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 + + def _finish_sub_step_edit(self, step_idx: int, sub_idx: int, editor: QLineEdit) -> None: + if not editor.isVisible(): + # Already finished/deleted + return + new_name = editor.text() + self.rename_proof_sub_step(new_name, step_idx, sub_idx) + editor.deleteLater() + self._active_sub_editor = None + + 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 + + def rename_proof_sub_step(self, new_name: str, step_index: int, sub_index: int) -> None: + from .commands import UndoableChange + step = self.model().steps[step_index] + if step.grouped_rewrites is None: + return + old_name = step.grouped_rewrites[sub_index].display_name + cmd = UndoableChange(self.graph_view, + lambda: self.model().rename_sub_step(step_index, sub_index, old_name), + lambda: self.model().rename_sub_step(step_index, sub_index, new_name)) + self.undo_stack.push(cmd) + def rename_proof_step(self, new_name: str, index: int) -> None: from .commands import UndoableChange old_name = self.model().steps[index].display_name @@ -602,6 +718,7 @@ def _step_info(self, index: Union[QModelIndex, QPersistentModelIndex]) -> tuple[ def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> None: painter.save() + painter.setRenderHint(QPainter.RenderHint.Antialiasing) is_grouped, is_expanded, grouped_rewrites = self._step_info(index) @@ -647,19 +764,31 @@ def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QM # ── Main timeline line ────────────────────────────────────────── is_last = index.row() == index.model().rowCount() - 1 - if is_last: - line_h = int(row_height / 2) - else: - line_h = int(option.rect.height()) # type: ignore[attr-defined] - line_rect = QRect( - self.line_padding, - int(option.rect.y()), # type: ignore[attr-defined] - self.line_width, - line_h - ) - painter.setPen(Qt.GlobalColor.transparent) - painter.setBrush(line_clr) - painter.drawRect(line_rect) + + # Use a Pen with RoundCap for lines to allow smooth overlaps with neighbor + # segments and the diverted path. + pen = QPen(line_clr, self.line_width) + pen.setCapStyle(Qt.PenCapStyle.RoundCap) + painter.setPen(pen) + painter.setBrush(Qt.GlobalColor.transparent) + + # Draw top half of line (to center of circle) + # We always draw this (it connects from the previous step) + circle_cy = option.rect.y() + row_height / 2 # type: ignore[attr-defined] + main_cx = self.line_padding + self.line_width / 2 + + # Draw line from top to center + # Start exactly at top edge. RoundCap will extend slightly above/below. + # This overlap ensures no gap with the previous item's bottom line. + painter.drawLine(QPointF(main_cx, option.rect.y()), QPointF(main_cx, circle_cy)) # type: ignore[attr-defined] + + # Draw bottom half of line (from center of circle to bottom) + # Only if NOT expanded (if expanded, the line diverts to the sub-steps) + if not is_expanded: + bottom_y = option.rect.y() + option.rect.height() # type: ignore[attr-defined] + if not is_last: + # Draw from center to bottom + painter.drawLine(QPointF(main_cx, circle_cy), QPointF(main_cx, bottom_y)) # ── Main circle ───────────────────────────────────────────────── circle_cy = option.rect.y() + row_height / 2 # type: ignore[attr-defined] @@ -735,7 +864,6 @@ def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QM painter.restore() - # ── Expanded sub-tree painting ────────────────────────────────────── def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, step_idx: int, grouped_rewrites: list['Rewrite'], row_height: int, @@ -745,37 +873,38 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, sub_tree_x = main_cx + self.sub_indent n = len(grouped_rewrites) - first_sub_top = option.rect.y() + row_height # type: ignore[attr-defined] - last_sub_cy = first_sub_top + (n - 1) * row_height + row_height / 2 + header_cy = option.rect.y() + row_height / 2 # type: ignore[attr-defined] + first_sub_cy = option.rect.y() + row_height + row_height / 2 # type: ignore[attr-defined] + last_sub_cy = option.rect.y() + row_height + (n - 1) * row_height + row_height / 2 # type: ignore[attr-defined] + bottom_y = option.rect.y() + option.rect.height() # type: ignore[attr-defined] - pen = QPen(line_clr, 2) + pen = QPen(line_clr, self.line_width) + pen.setCapStyle(Qt.PenCapStyle.RoundCap) painter.setPen(pen) + painter.setBrush(Qt.GlobalColor.transparent) - # Diagonal connector from main circle down to start of sub-tree - header_cy = option.rect.y() + row_height / 2 # type: ignore[attr-defined] - painter.drawLine( - QPointF(main_cx, header_cy + self.circle_radius_selected), - QPointF(sub_tree_x, first_sub_top) - ) + # Path connecting header -> sub-steps -> next step + path = QPainterPath() + # Start at the headers circle + path.moveTo(main_cx, header_cy) + # Line to first sub-step + path.lineTo(sub_tree_x, first_sub_cy) + # Line down to last sub-step + path.lineTo(sub_tree_x, last_sub_cy) + # Line back to main axis at the bottom + path.lineTo(main_cx, bottom_y) - # Sub-tree vertical line - painter.drawLine( - QPointF(sub_tree_x, first_sub_top), - QPointF(sub_tree_x, last_sub_cy) - ) + painter.drawPath(path) - # Determine which sub-step is selected (if any) - view = self.parent() - selected_sub_idx = -1 - if isinstance(view, ProofStepView) and view.selected_sub_step is not None: - sel_step_idx, sel_sub_idx = view.selected_sub_step - if step_idx == sel_step_idx: - selected_sub_idx = sel_sub_idx - - sub_circle_cx = sub_tree_x + self.sub_branch_len for i, sub_step in enumerate(grouped_rewrites): - sub_cy = first_sub_top + i * row_height + row_height / 2 - is_sub_selected = (i == selected_sub_idx) + sub_cy = first_sub_cy + i * row_height + is_sub_selected = False + # Determine which sub-step is selected (if any) + view = self.parent() + if isinstance(view, ProofStepView) and view.selected_sub_step is not None: + sel_step_idx, sel_sub_idx = view.selected_sub_step + if step_idx == sel_step_idx and i == sel_sub_idx: + is_sub_selected = True # Check if this sub-step is being hovered (for individual hover effect) is_sub_hovered = (self.hover_step_idx == step_idx and self.hover_sub_idx == i) @@ -794,22 +923,15 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, else: painter.setBrush(QColor(229, 243, 255)) highlight_rect = QRect( - int(sub_tree_x - 4), + int(sub_tree_x - 10), int(sub_cy - row_height / 2), - int(option.rect.width() - sub_tree_x + 4), # type: ignore[attr-defined] + int(option.rect.width() - sub_tree_x + 10), # type: ignore[attr-defined] row_height ) painter.drawRect(highlight_rect) - # Horizontal branch - painter.setPen(pen) - painter.drawLine( - QPointF(sub_tree_x, sub_cy), - QPointF(sub_circle_cx - self.sub_circle_radius, sub_cy) - ) - # Sub-step circle - painter.setPen(QPen(line_clr, 2)) + painter.setPen(QPen(line_clr, self.line_width)) if is_sub_selected: painter.setBrush(QColor(30, 100, 200)) # brighter blue when selected r = self.sub_circle_radius + 1 @@ -817,11 +939,11 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, painter.setBrush(QColor(70, 130, 180)) # default steel-blue r = self.sub_circle_radius painter.drawEllipse( - QPointF(sub_circle_cx, sub_cy), r, r + QPointF(sub_tree_x, sub_cy), r, r ) # Sub-step text - sub_text_x = int(sub_circle_cx + self.sub_circle_radius + 8) + sub_text_x = int(sub_tree_x + self.sub_circle_radius + 10) sub_text_rect = QRect( sub_text_x, int(sub_cy - text_height / 2), From bd7e8ecae99bf8c8e0c215d0312f49e1c3a0a0cf Mon Sep 17 00:00:00 2001 From: axif Date: Tue, 24 Feb 2026 03:59:08 +0600 Subject: [PATCH 05/19] Refactor imports and clean up whitespace in proof, rewrite_action, rewrite_data, and unfusion_rewrite modules --- zxlive/proof.py | 34 +++++++++++++++++----------------- zxlive/rewrite_action.py | 8 ++++---- zxlive/rewrite_data.py | 1 + zxlive/unfusion_rewrite.py | 3 +++ 4 files changed, 25 insertions(+), 21 deletions(-) diff --git a/zxlive/proof.py b/zxlive/proof.py index 2c91c55c..5de14322 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -6,9 +6,9 @@ from PySide6.QtCore import (QAbstractItemModel, QAbstractListModel, QItemSelection, QModelIndex, QPersistentModelIndex, - QPoint, QPointF, QRect, QRectF, QSize, Qt) + QPoint, QPointF, QRect, QSize, Qt) from PySide6.QtGui import QColor, QFont, QFontMetrics, QMouseEvent, QPainter, QPainterPath, QPen, QPolygonF -from PySide6.QtWidgets import (QAbstractItemView, QInputDialog, QLineEdit, QListView, QMenu, +from PySide6.QtWidgets import (QAbstractItemView, QLineEdit, QListView, QMenu, QStyle, QStyledItemDelegate, QStyleOptionViewItem, QWidget) @@ -191,13 +191,13 @@ def rename_sub_step(self, step_index: int, sub_index: int, name: str) -> None: old_sub_step = grouped[sub_index] new_sub_step = Rewrite(name, old_sub_step.rule, old_sub_step.graph, old_sub_step.grouped_rewrites) - + new_grouped = list(grouped) new_grouped[sub_index] = new_sub_step # Update the main step's grouped rewrites self.steps[step_index] = Rewrite(old_step.display_name, old_step.rule, old_step.graph, new_grouped) - + # Rerender modelIndex = self.createIndex(step_index, 0) self.dataChanged.emit(modelIndex, modelIndex, []) @@ -520,7 +520,7 @@ def show_context_menu(self, position: QPoint) -> None: if self.model().steps[index - 1].grouped_rewrites is not None: ungroup_action = context_menu.addAction("Ungroup Steps") action_function_map[ungroup_action] = self.ungroup_selected_step - + # Check if we clicked on a sub-step step_idx = index - 1 if step_idx in self.expanded_groups: @@ -551,7 +551,7 @@ def _open_sub_step_editor(self, step_idx: int, sub_idx: int) -> None: # 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) @@ -559,44 +559,44 @@ def _open_sub_step_editor(self, step_idx: int, sub_idx: int) -> None: 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.sub_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_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; }") + 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; }") + 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 def _finish_sub_step_edit(self, step_idx: int, sub_idx: int, editor: QLineEdit) -> None: - if not editor.isVisible(): + if not editor.isVisible(): # Already finished/deleted return new_name = editor.text() diff --git a/zxlive/rewrite_action.py b/zxlive/rewrite_action.py index bc2f9fbc..6c0229a5 100644 --- a/zxlive/rewrite_action.py +++ b/zxlive/rewrite_action.py @@ -8,7 +8,7 @@ from typing import TYPE_CHECKING, cast, Union, Optional from concurrent.futures import ThreadPoolExecutor -from pyzx.rewrite import Rewrite, RewriteSingleVertex, RewriteDoubleVertex, RewriteSimpGraph +from pyzx.rewrite import Rewrite, RewriteSingleVertex, RewriteDoubleVertex from PySide6.QtCore import (Qt, QAbstractItemModel, QModelIndex, QPersistentModelIndex, Signal, QObject, QMetaObject, QIODevice, QBuffer, QPoint, QPointF, QLineF) @@ -104,7 +104,7 @@ def do_rewrite(self, panel: ProofPanel) -> None: matches = [v for v in verts if rule_sv.is_match(g, v)] elif self.match_type == MATCH_DOUBLE: matches = [g.edge_st(e) for e in edges if g.edge_st(e)[0] != g.edge_st(e)[1] and self.rule.is_match(g, *g.edge_st(e))] # type: ignore[attr-defined] - elif self.match_type == MATCH_COMPOUND: # We don't necessarily have a matcher in this case + elif self.match_type == MATCH_COMPOUND: # We don't necessarily have a matcher in this case # if self.rule.is_match(g, verts): if len(verts) == 0: matches = [list(g.vertices())] # type: ignore @@ -117,7 +117,6 @@ def do_rewrite(self, panel: ProofPanel) -> None: applied = False for m in matches: if self.match_type == MATCH_DOUBLE: - rule_dv = cast(RewriteDoubleVertex, self.rule) v1, v2 = cast(tuple[VT, VT], m) if self.rule.apply(g, v1, v2): # type: ignore[attr-defined] applied = True @@ -146,7 +145,8 @@ def apply_rewrite(self, g: GraphT, matches: list) -> tuple[GraphT, list[VT]]: if self.match_type == MATCH_DOUBLE: v1, v2 = cast(tuple[VT, VT], m) self.rule.apply(g, v1, v2) # type: ignore[attr-defined] - else: self.rule.apply(g, m) # type: ignore[attr-defined] + else: + self.rule.apply(g, m) # type: ignore[attr-defined] # rewrite = self.rule(g, matches) # assert isinstance(rewrite, tuple) and len(rewrite) == 4 # etab, rem_verts, rem_edges, check_isolated_vertices = rewrite diff --git a/zxlive/rewrite_data.py b/zxlive/rewrite_data.py index 35abd98c..1064853c 100644 --- a/zxlive/rewrite_data.py +++ b/zxlive/rewrite_data.py @@ -134,6 +134,7 @@ def rule(g: GraphT, matches: list) -> bool: return CustomRule(subgraph, simplified, "", "").applier(g, matches) return RewriteSimpGraph(rule, rule) # type: ignore[arg-type] + def create_subgraph_with_boundary(graph: GraphT, verts: list[VT]) -> GraphT: verts = [v for v in verts if graph.type(v) != VertexType.BOUNDARY] subgraph = cast(GraphT, graph.subgraph_from_vertices(verts)) diff --git a/zxlive/unfusion_rewrite.py b/zxlive/unfusion_rewrite.py index 7bfb39fb..0b4ea8cb 100644 --- a/zxlive/unfusion_rewrite.py +++ b/zxlive/unfusion_rewrite.py @@ -34,6 +34,7 @@ def apply_unfuse_rule(graph: BaseGraph[VT, ET], vertices: list[VT]) -> bool: raise NotImplementedError("Interactive unfusion should be handled by UnfusionRewriteAction.") return True + def unfuse_rule_simp_applier(graph: BaseGraph[VT, ET]) -> bool: """A no-op simplification applier for the unfusion rule.""" # This function should not be called directly for the interactive unfusion @@ -42,9 +43,11 @@ def unfuse_rule_simp_applier(graph: BaseGraph[VT, ET]) -> bool: raise NotImplementedError("Interactive unfusion should be handled by UnfusionRewriteAction.") return True + unfusion_rewrite: RewriteSimpGraph[VT, ET] = RewriteSimpGraph(apply_unfuse_rule, unfuse_rule_simp_applier) unfusion_rewrite.is_match = match_unfuse_single_vertex # type: ignore[attr-defined] + class UnfusionRewriteAction: """Special rewrite action that handles the interactive unfusion process.""" From 003215fe0b58c3c8266e333d8d604c99b796c56e Mon Sep 17 00:00:00 2001 From: axif Date: Wed, 25 Feb 2026 17:27:53 +0600 Subject: [PATCH 06/19] Refactor proof step rendering to differentiate between hovering over grouped step headers and sub-steps, improving hover and selection highlighting. --- zxlive/proof.py | 172 ++++++++++++++++++++----------------- zxlive/rewrite_action.py | 45 ++++------ zxlive/rewrite_data.py | 8 +- zxlive/unfusion_rewrite.py | 37 ++++---- 4 files changed, 134 insertions(+), 128 deletions(-) diff --git a/zxlive/proof.py b/zxlive/proof.py index 5de14322..b1b1f35d 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -114,12 +114,12 @@ def columnCount(self, index: Union[QModelIndex, QPersistentModelIndex] = QModelI """The number of columns""" return 1 - def rowCount(self, parent: Union[QModelIndex, QPersistentModelIndex] = QModelIndex()) -> int: + def rowCount(self, index: 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 parent or not parent.isValid(): + if not index or not index.isValid(): return len(self.steps) + 1 else: return 0 @@ -369,12 +369,7 @@ def _triangle_hit_test(self, step_idx: int, event_pos_x: int, event_pos_y: int, return (text_x_base <= click_x <= text_x_base + tri_size * 2 and tri_cy - tri_size <= click_y <= tri_cy + tri_size) - def _get_sub_step_hover(self, step_idx: int, event_pos_y: int, rect_y: int) -> int: - """Determine which sub-step the mouse is hovering over in an expanded group. - Returns the 0-based sub-step index, or -1 if not hovering over a sub-step. - """ - return self._sub_step_hit_test(step_idx, event_pos_y, rect_y) def _navigate_to_sub_step(self, step_idx: int, sub_idx: int) -> None: """Display the graph corresponding to a sub-step within a grouped rewrite.""" @@ -433,6 +428,10 @@ def mousePressEvent(self, event: QMouseEvent) -> None: # type: ignore[override] if toggle_idx >= 0: self.toggle_group_expansion(toggle_idx) + def _repaint_step(self, step_idx: int) -> None: + """Trigger repaint for a step row by its 0-based step index.""" + self.update(self.model().index(step_idx + 1, 0)) + def mouseMoveEvent(self, event: QMouseEvent) -> None: # type: ignore[override] """Track which sub-step the mouse is hovering over and trigger repaint.""" delegate = self.itemDelegate() @@ -442,37 +441,45 @@ def mouseMoveEvent(self, event: QMouseEvent) -> None: # type: ignore[override] old_step = delegate.hover_step_idx old_sub = delegate.hover_sub_idx + old_header = delegate.hover_header_step_idx new_step = -1 new_sub = -1 + new_header = -1 index = self.indexAt(event.pos()) 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 - and 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 - new_sub = sub_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 + new_sub = sub_idx + else: + new_header = step_idx + else: + new_header = step_idx if new_step != old_step or new_sub != old_sub: delegate.hover_step_idx = new_step delegate.hover_sub_idx = new_sub - # Repaint the old hovered item if old_step >= 0: - old_idx = self.model().index(old_step + 1, 0) - self.update(old_idx) - # Repaint the new hovered item + self._repaint_step(old_step) if new_step >= 0: - new_idx = self.model().index(new_step + 1, 0) - self.update(new_idx) + self._repaint_step(new_step) + + if new_header != old_header: + delegate.hover_header_step_idx = new_header + if old_header >= 0: + self._repaint_step(old_header) + if new_header >= 0: + self._repaint_step(new_header) - # Change cursor to pointing hand when hovering over a clickable sub-step if new_sub >= 0: self.setCursor(Qt.CursorShape.PointingHandCursor) else: @@ -485,11 +492,14 @@ def leaveEvent(self, event: Any) -> None: delegate = self.itemDelegate() if isinstance(delegate, ProofStepItemDelegate): old_step = delegate.hover_step_idx + old_header = delegate.hover_header_step_idx delegate.hover_step_idx = -1 delegate.hover_sub_idx = -1 + delegate.hover_header_step_idx = -1 if old_step >= 0: - old_idx = self.model().index(old_step + 1, 0) - self.update(old_idx) + self._repaint_step(old_step) + if old_header >= 0: + self._repaint_step(old_header) self.unsetCursor() super().leaveEvent(event) @@ -604,10 +614,6 @@ def _finish_sub_step_edit(self, step_idx: int, sub_idx: int, editor: QLineEdit) editor.deleteLater() self._active_sub_editor = None - 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 def rename_proof_sub_step(self, new_name: str, step_index: int, sub_index: int) -> None: from .commands import UndoableChange @@ -698,6 +704,8 @@ class ProofStepItemDelegate(QStyledItemDelegate): # Track hover position for sub-steps hover_step_idx: int = -1 hover_sub_idx: int = -1 + # Track hover over group header + hover_header_step_idx: int = -1 def _step_info(self, index: Union[QModelIndex, QPersistentModelIndex]) -> tuple[bool, bool, Optional[list['Rewrite']]]: """Return (is_grouped, is_expanded, grouped_rewrites) for a given row.""" @@ -716,6 +724,25 @@ def _step_info(self, index: Union[QModelIndex, QPersistentModelIndex]) -> tuple[ is_expanded = isinstance(view, ProofStepView) and step_idx in view.expanded_groups return True, is_expanded, step.grouped_rewrites + @staticmethod + def _bg_color(selected: bool, sub_selected: bool, hovered: bool) -> QColor: + """Return the background color for the given state.""" + if display_setting.dark_mode: + if selected: + return QColor(60, 80, 120) + if sub_selected: + return QColor(45, 50, 60) + if hovered: + return QColor(50, 60, 80) + return QColor(35, 39, 46) + if selected: + return QColor(204, 232, 255) + if sub_selected: + return QColor(240, 245, 250) + if hovered: + return QColor(229, 243, 255) + return QColor(255, 255, 255) + def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> None: painter.save() painter.setRenderHint(QPainter.RenderHint.Antialiasing) @@ -737,30 +764,29 @@ def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QM has_selected_sub_step = True # ── Background ────────────────────────────────────────────────── + is_selected = bool(option.state & QStyle.StateFlag.State_Selected) # type: ignore[attr-defined] + is_mouse_over = bool(option.state & QStyle.StateFlag.State_MouseOver) # type: ignore[attr-defined] + is_header_hovered = (is_grouped + and index.row() > 0 + and self.hover_header_step_idx == index.row() - 1) + + bg = self._bg_color(is_selected, has_selected_sub_step, is_mouse_over) + neutral_bg = self._bg_color(False, False, False) + painter.setPen(Qt.GlobalColor.transparent) - if display_setting.dark_mode: - if option.state & QStyle.StateFlag.State_Selected: # type: ignore[attr-defined] - painter.setBrush(QColor(60, 80, 120)) - elif has_selected_sub_step: - # Lighter background when a sub-step is selected - painter.setBrush(QColor(45, 50, 60)) - elif option.state & QStyle.StateFlag.State_MouseOver and not is_expanded: # type: ignore[attr-defined] - # Only hover highlight if not expanded (sub-steps handle their own hover) - painter.setBrush(QColor(50, 60, 80)) - else: - painter.setBrush(QColor(35, 39, 46)) + if is_expanded: + # Fill entire area with neutral, then highlight just the header row + painter.setBrush(neutral_bg) + painter.drawRect(option.rect) # type: ignore[attr-defined] + if is_selected or has_selected_sub_step or is_header_hovered: + header_bg = self._bg_color(is_selected, has_selected_sub_step, is_header_hovered) + painter.setBrush(header_bg) + painter.drawRect(QRect( + option.rect.x(), option.rect.y(), # type: ignore[attr-defined] + option.rect.width(), row_height)) # type: ignore[attr-defined] else: - if option.state & QStyle.StateFlag.State_Selected: # type: ignore[attr-defined] - painter.setBrush(QColor(204, 232, 255)) - elif has_selected_sub_step: - # Lighter background when a sub-step is selected - painter.setBrush(QColor(240, 245, 250)) - elif option.state & QStyle.StateFlag.State_MouseOver and not is_expanded: # type: ignore[attr-defined] - # Only hover highlight if not expanded (sub-steps handle their own hover) - painter.setBrush(QColor(229, 243, 255)) - else: - painter.setBrush(Qt.GlobalColor.white) - painter.drawRect(option.rect) # type: ignore[attr-defined] + painter.setBrush(bg) + painter.drawRect(option.rect) # type: ignore[attr-defined] # ── Main timeline line ────────────────────────────────────────── is_last = index.row() == index.model().rowCount() - 1 @@ -772,22 +798,26 @@ def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QM painter.setPen(pen) painter.setBrush(Qt.GlobalColor.transparent) - # Draw top half of line (to center of circle) - # We always draw this (it connects from the previous step) circle_cy = option.rect.y() + row_height / 2 # type: ignore[attr-defined] main_cx = self.line_padding + self.line_width / 2 # Draw line from top to center - # Start exactly at top edge. RoundCap will extend slightly above/below. - # This overlap ensures no gap with the previous item's bottom line. painter.drawLine(QPointF(main_cx, option.rect.y()), QPointF(main_cx, circle_cy)) # type: ignore[attr-defined] + # For expanded groups, draw the sub-tree BEFORE the circle so the + # path doesn't draw over the circle. + if is_expanded and grouped_rewrites: + self._paint_sub_tree(painter, option, index.row() - 1, + grouped_rewrites, + row_height, text_height, font, fg, line_clr) + # Draw bottom half of line (from center of circle to bottom) # Only if NOT expanded (if expanded, the line diverts to the sub-steps) if not is_expanded: bottom_y = option.rect.y() + option.rect.height() # type: ignore[attr-defined] if not is_last: - # Draw from center to bottom + painter.setPen(pen) + painter.setBrush(Qt.GlobalColor.transparent) painter.drawLine(QPointF(main_cx, circle_cy), QPointF(main_cx, bottom_y)) # ── Main circle ───────────────────────────────────────────────── @@ -841,11 +871,7 @@ def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QM painter.setPen(fg) painter.drawText(text_rect, Qt.AlignmentFlag.AlignLeft, header_text) - # Draw expanded sub-tree - if is_expanded and grouped_rewrites: - self._paint_sub_tree(painter, option, index.row() - 1, - grouped_rewrites, - row_height, text_height, font, fg, line_clr) + # Sub-tree was already drawn above (before the circle) for expanded groups else: # Regular (non-grouped) step text text = index.data(Qt.ItemDataRole.DisplayRole) @@ -909,26 +935,14 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, # Check if this sub-step is being hovered (for individual hover effect) is_sub_hovered = (self.hover_step_idx == step_idx and self.hover_sub_idx == i) - # Draw highlight background for selected or hovered sub-step + # Highlight starts AFTER the branch line (matching ungrouped style) if is_sub_selected or is_sub_hovered: painter.setPen(Qt.GlobalColor.transparent) - if is_sub_selected: - if display_setting.dark_mode: - painter.setBrush(QColor(50, 90, 140, 120)) - else: - painter.setBrush(QColor(180, 215, 255, 160)) - elif is_sub_hovered: - if display_setting.dark_mode: - painter.setBrush(QColor(50, 60, 80)) - else: - painter.setBrush(QColor(229, 243, 255)) - highlight_rect = QRect( - int(sub_tree_x - 10), - int(sub_cy - row_height / 2), - int(option.rect.width() - sub_tree_x + 10), # type: ignore[attr-defined] - row_height - ) - painter.drawRect(highlight_rect) + painter.setBrush(self._bg_color(is_sub_selected, False, is_sub_hovered)) + hl_left = int(sub_tree_x + self.sub_circle_radius + 2) + painter.drawRect(QRect( + hl_left, int(sub_cy - row_height / 2), + int(option.rect.width() - hl_left), row_height)) # type: ignore[attr-defined] # Sub-step circle painter.setPen(QPen(line_clr, self.line_width)) diff --git a/zxlive/rewrite_action.py b/zxlive/rewrite_action.py index 6c0229a5..121e1fd5 100644 --- a/zxlive/rewrite_action.py +++ b/zxlive/rewrite_action.py @@ -8,7 +8,7 @@ from typing import TYPE_CHECKING, cast, Union, Optional from concurrent.futures import ThreadPoolExecutor -from pyzx.rewrite import Rewrite, RewriteSingleVertex, RewriteDoubleVertex +from pyzx.rewrite import Rewrite, RewriteSingleVertex, RewriteDoubleVertex, RewriteSimpGraph from PySide6.QtCore import (Qt, QAbstractItemModel, QModelIndex, QPersistentModelIndex, Signal, QObject, QMetaObject, QIODevice, QBuffer, QPoint, QPointF, QLineF) @@ -103,9 +103,11 @@ def do_rewrite(self, panel: ProofPanel) -> None: rule_sv = cast(RewriteSingleVertex, self.rule) matches = [v for v in verts if rule_sv.is_match(g, v)] elif self.match_type == MATCH_DOUBLE: - matches = [g.edge_st(e) for e in edges if g.edge_st(e)[0] != g.edge_st(e)[1] and self.rule.is_match(g, *g.edge_st(e))] # type: ignore[attr-defined] + rule_dv = cast(RewriteDoubleVertex, self.rule) + matches = [g.edge_st(e) for e in edges + if g.edge_st(e)[0] != g.edge_st(e)[1] + and rule_dv.is_match(g, *g.edge_st(e))] elif self.match_type == MATCH_COMPOUND: # We don't necessarily have a matcher in this case - # if self.rule.is_match(g, verts): if len(verts) == 0: matches = [list(g.vertices())] # type: ignore else: @@ -117,11 +119,18 @@ def do_rewrite(self, panel: ProofPanel) -> None: applied = False for m in matches: if self.match_type == MATCH_DOUBLE: + rule_dv = cast(RewriteDoubleVertex, self.rule) v1, v2 = cast(tuple[VT, VT], m) - if self.rule.apply(g, v1, v2): # type: ignore[attr-defined] + if rule_dv.apply(g, v1, v2): + applied = True + elif self.match_type == MATCH_SINGLE: + rule_sv = cast(RewriteSingleVertex, self.rule) + if rule_sv.apply(g, cast(VT, m)): + applied = True + else: + rule_sg = cast(RewriteSimpGraph, self.rule) + if rule_sg.apply(g, cast(list[VT], m)): applied = True - elif self.rule.apply(g, m): # type: ignore[attr-defined] - applied = True # g, rem_verts = self.apply_rewrite(g, matches) # rem_verts_list.extend(rem_verts) except Exception as ex: @@ -134,28 +143,6 @@ def do_rewrite(self, panel: ProofPanel) -> None: 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. - def apply_rewrite(self, g: GraphT, matches: list) -> tuple[GraphT, list[VT]]: - if self.returns_new_graph: - graph = self.rule(g, matches) # type: ignore[call-arg] - assert isinstance(graph, GraphT) - return graph, [] - - for m in matches: - if self.match_type == MATCH_DOUBLE: - v1, v2 = cast(tuple[VT, VT], m) - self.rule.apply(g, v1, v2) # type: ignore[attr-defined] - else: - self.rule.apply(g, m) # type: ignore[attr-defined] - # rewrite = self.rule(g, matches) - # assert isinstance(rewrite, tuple) and len(rewrite) == 4 - # etab, rem_verts, rem_edges, check_isolated_vertices = rewrite - # g.remove_edges(rem_edges) - # g.remove_vertices(rem_verts) - # g.add_edge_table(etab) - # return g, rem_verts - return g, [] - def update_active(self, g: GraphT, verts: list[VT], edges: list[ET]) -> None: if self.copy_first: g = copy.deepcopy(g) @@ -521,4 +508,4 @@ def refresh_rewrites_model(self) -> None: if index.data() in expanded_indexes: self.expand(index) self.clicked.connect(model.do_rewrite) - self.proof_panel.graph_scene.selection_changed_custom.connect(lambda: model.executor.submit(model.update_on_selection)) + self.proof_panel.graph_scene.selection_changed_custom.connect(lambda: model.executor.submit(model.update_on_selection)) \ No newline at end of file diff --git a/zxlive/rewrite_data.py b/zxlive/rewrite_data.py index 1064853c..14a7b095 100644 --- a/zxlive/rewrite_data.py +++ b/zxlive/rewrite_data.py @@ -132,7 +132,11 @@ def rule(g: GraphT, matches: list) -> bool: simplified = cast(GraphT, subgraph.copy()) strategy(simplified) return CustomRule(subgraph, simplified, "", "").applier(g, matches) - return RewriteSimpGraph(rule, rule) # type: ignore[arg-type] + + def simp_rule(g: GraphT) -> bool: + strategy(g) + return True + return RewriteSimpGraph(rule, simp_rule) # type: ignore[arg-type] def create_subgraph_with_boundary(graph: GraphT, verts: list[VT]) -> GraphT: @@ -352,4 +356,4 @@ def refresh_custom_rules() -> None: action_groups["Custom rules"] = {rule["text"]: rule for rule in read_custom_rules()} -refresh_custom_rules() +refresh_custom_rules() \ No newline at end of file diff --git a/zxlive/unfusion_rewrite.py b/zxlive/unfusion_rewrite.py index 0b4ea8cb..26393ef9 100644 --- a/zxlive/unfusion_rewrite.py +++ b/zxlive/unfusion_rewrite.py @@ -26,26 +26,27 @@ def match_unfuse_single_vertex(graph: GraphT, vertices: list[VT]) -> list[VT]: return [] -def apply_unfuse_rule(graph: BaseGraph[VT, ET], vertices: list[VT]) -> bool: - """Apply the unfusion rule to a single vertex.""" - # This function should not be called directly for the interactive unfusion - # It's here for compatibility with the rewrite system structure - # The actual unfusion logic is handled by the UnfusionRewriteAction - raise NotImplementedError("Interactive unfusion should be handled by UnfusionRewriteAction.") - return True +class UnfusionRewrite(RewriteSimpGraph[VT, ET]): + """RewriteSimpGraph subclass with an is_match method for unfusion. + The actual unfusion logic is handled interactively by UnfusionRewriteAction, + so apply/simp just raise NotImplementedError. + """ -def unfuse_rule_simp_applier(graph: BaseGraph[VT, ET]) -> bool: - """A no-op simplification applier for the unfusion rule.""" - # This function should not be called directly for the interactive unfusion - # It's here for compatibility with the rewrite system structure - # The actual unfusion logic is handled by the UnfusionRewriteAction - raise NotImplementedError("Interactive unfusion should be handled by UnfusionRewriteAction.") - return True + def __init__(self) -> None: + def _no_op_applier(graph: BaseGraph[VT, ET], vertices: list[VT]) -> bool: + raise NotImplementedError("Interactive unfusion should be handled by UnfusionRewriteAction.") + def _no_op_simp(graph: BaseGraph[VT, ET]) -> bool: + raise NotImplementedError("Interactive unfusion should be handled by UnfusionRewriteAction.") -unfusion_rewrite: RewriteSimpGraph[VT, ET] = RewriteSimpGraph(apply_unfuse_rule, unfuse_rule_simp_applier) -unfusion_rewrite.is_match = match_unfuse_single_vertex # type: ignore[attr-defined] + super().__init__(_no_op_applier, _no_op_simp) + + def is_match(self, graph: GraphT, vertices: list[VT]) -> bool: # type: ignore[override] + return bool(match_unfuse_single_vertex(graph, vertices)) + + +unfusion_rewrite: UnfusionRewrite = UnfusionRewrite() class UnfusionRewriteAction: @@ -168,7 +169,7 @@ def reassign_edges(edges: list[ET], node: VT) -> None: from .rewrite_data import rules_basic cmd = AddRewriteStep(self.proof_panel.graph_view, new_g, - self.proof_panel.step_view, str(rules_basic['unfuse']['text'])) + self.proof_panel.step_view, rules_basic['unfuse']['text']) anim = anims.unfuse(graph, new_g, original_vertex, self.proof_panel.graph_scene) self.proof_panel.undo_stack.push(cmd, anim_after=anim) @@ -183,4 +184,4 @@ def _cleanup(self) -> None: try: self.proof_panel.graph_scene.selection_changed_custom.disconnect(self._on_selection_changed) except RuntimeError: - pass # Connection might not exist + pass # Connection might not exist \ No newline at end of file From 070fb64394d8c4e1ec23f7fa9570f2279027dc39 Mon Sep 17 00:00:00 2001 From: axif Date: Wed, 25 Feb 2026 17:29:59 +0600 Subject: [PATCH 07/19] add missing `end line` at the end --- zxlive/rewrite_action.py | 2 +- zxlive/rewrite_data.py | 2 +- zxlive/unfusion_rewrite.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/zxlive/rewrite_action.py b/zxlive/rewrite_action.py index 121e1fd5..c245a754 100644 --- a/zxlive/rewrite_action.py +++ b/zxlive/rewrite_action.py @@ -508,4 +508,4 @@ def refresh_rewrites_model(self) -> None: if index.data() in expanded_indexes: self.expand(index) self.clicked.connect(model.do_rewrite) - self.proof_panel.graph_scene.selection_changed_custom.connect(lambda: model.executor.submit(model.update_on_selection)) \ No newline at end of file + self.proof_panel.graph_scene.selection_changed_custom.connect(lambda: model.executor.submit(model.update_on_selection)) diff --git a/zxlive/rewrite_data.py b/zxlive/rewrite_data.py index 14a7b095..00f822b0 100644 --- a/zxlive/rewrite_data.py +++ b/zxlive/rewrite_data.py @@ -356,4 +356,4 @@ def refresh_custom_rules() -> None: action_groups["Custom rules"] = {rule["text"]: rule for rule in read_custom_rules()} -refresh_custom_rules() \ No newline at end of file +refresh_custom_rules() diff --git a/zxlive/unfusion_rewrite.py b/zxlive/unfusion_rewrite.py index 26393ef9..69d06cfe 100644 --- a/zxlive/unfusion_rewrite.py +++ b/zxlive/unfusion_rewrite.py @@ -184,4 +184,4 @@ def _cleanup(self) -> None: try: self.proof_panel.graph_scene.selection_changed_custom.disconnect(self._on_selection_changed) except RuntimeError: - pass # Connection might not exist \ No newline at end of file + pass # Connection might not exist From b40ea25e570f827bdd102b9771fdc27be8f829a0 Mon Sep 17 00:00:00 2001 From: axif Date: Wed, 25 Feb 2026 18:42:49 +0600 Subject: [PATCH 08/19] feat: Introduce functionality to modify and undo/redo changes for individual sub-steps within grouped proof steps. --- zxlive/commands.py | 27 +++++++++++++++++++++++---- zxlive/proof.py | 32 +++++++++++++++++++++++++++----- 2 files changed, 50 insertions(+), 9 deletions(-) diff --git a/zxlive/commands.py b/zxlive/commands.py index ec726558..d08362e6 100644 --- a/zxlive/commands.py +++ b/zxlive/commands.py @@ -69,16 +69,35 @@ def __init__(self, command: BaseCommand, step_view: ProofStepView): self.command = command self.step_view = step_view self.proof_step_index = int(step_view.currentIndex().row()) + self.sub_step = step_view.selected_sub_step def undo(self) -> None: - self.step_view.move_to_step(self.proof_step_index) + 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() - self.step_view.model().set_graph(self.proof_step_index, self.command.g) + 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: - self.step_view.move_to_step(self.proof_step_index) + 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.redo() - self.step_view.model().set_graph(self.proof_step_index, self.command.g) + 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) @dataclass diff --git a/zxlive/proof.py b/zxlive/proof.py index b1b1f35d..7e9b96b1 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -77,9 +77,31 @@ def set_graph(self, index: int, graph: GraphT) -> None: self.initial_graph = graph else: old_step = self.steps[index - 1] - new_step = Rewrite(old_step.display_name, old_step.rule, graph) + new_step = Rewrite(old_step.display_name, old_step.rule, graph, old_step.grouped_rewrites) self.steps[index - 1] = new_step + # Rerender to ensure the model reflects the change immediately + modelIndex = self.createIndex(index, 0) + self.dataChanged.emit(modelIndex, modelIndex, []) + + def set_sub_graph(self, step_idx: int, sub_idx: int, graph: GraphT) -> None: + old_step = self.steps[step_idx] + grouped = old_step.grouped_rewrites + if grouped is None or sub_idx >= len(grouped): + return + + old_sub_step = grouped[sub_idx] + new_sub_step = Rewrite(old_sub_step.display_name, old_sub_step.rule, graph, old_sub_step.grouped_rewrites) + + new_grouped = list(grouped) + new_grouped[sub_idx] = new_sub_step + + self.steps[step_idx] = Rewrite(old_step.display_name, old_step.rule, old_step.graph, new_grouped) + + # Rerender + modelIndex = self.createIndex(step_idx + 1, 0) + self.dataChanged.emit(modelIndex, modelIndex, []) + def graphs(self) -> list[GraphT]: return [self.initial_graph] + [step.graph for step in self.steps] @@ -179,7 +201,7 @@ def rename_step(self, index: int, name: str) -> None: # Rerender the proof step otherwise it will display the old name until # the cursor moves - modelIndex = self.createIndex(index, 0) + modelIndex = self.createIndex(index + 1, 0) self.dataChanged.emit(modelIndex, modelIndex, []) def rename_sub_step(self, step_index: int, sub_index: int, name: str) -> None: @@ -199,7 +221,7 @@ def rename_sub_step(self, step_index: int, sub_index: int, name: str) -> None: self.steps[step_index] = Rewrite(old_step.display_name, old_step.rule, old_step.graph, new_grouped) # Rerender - modelIndex = self.createIndex(step_index, 0) + modelIndex = self.createIndex(step_index + 1, 0) self.dataChanged.emit(modelIndex, modelIndex, []) def group_steps(self, start_index: int, end_index: int) -> None: @@ -213,7 +235,7 @@ def group_steps(self, start_index: int, end_index: int) -> None: for _ in range(end_index - start_index + 1): self.pop_rewrite(start_index)[0] self.add_rewrite(new_rewrite, start_index) - modelIndex = self.createIndex(start_index, 0) + modelIndex = self.createIndex(start_index + 1, 0) self.dataChanged.emit(modelIndex, modelIndex, []) def ungroup_steps(self, index: int) -> None: @@ -224,7 +246,7 @@ def ungroup_steps(self, index: int) -> None: self.pop_rewrite(index) for i, step in enumerate(individual_steps): self.add_rewrite(step, index + i) - self.dataChanged.emit(self.createIndex(index, 0), + self.dataChanged.emit(self.createIndex(index + 1, 0), self.createIndex(index + len(individual_steps), 0), []) From e334dcf6a24ac0b1d0ee65f5f12fb274f27ea86b Mon Sep 17 00:00:00 2001 From: axif Date: Wed, 25 Feb 2026 18:44:51 +0600 Subject: [PATCH 09/19] removed blank space from proof --- zxlive/proof.py | 3 --- 1 file changed, 3 deletions(-) diff --git a/zxlive/proof.py b/zxlive/proof.py index 7e9b96b1..c0969147 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -391,8 +391,6 @@ def _triangle_hit_test(self, step_idx: int, event_pos_x: int, event_pos_y: int, return (text_x_base <= click_x <= text_x_base + tri_size * 2 and tri_cy - tri_size <= click_y <= tri_cy + tri_size) - - def _navigate_to_sub_step(self, step_idx: int, sub_idx: int) -> None: """Display the graph corresponding to a sub-step within a grouped rewrite.""" step = self.model().steps[step_idx] @@ -636,7 +634,6 @@ def _finish_sub_step_edit(self, step_idx: int, sub_idx: int, editor: QLineEdit) editor.deleteLater() self._active_sub_editor = None - def rename_proof_sub_step(self, new_name: str, step_index: int, sub_index: int) -> None: from .commands import UndoableChange step = self.model().steps[step_index] From 2979bf134a21dc39c3cb4359848f8dd80ca2e99d Mon Sep 17 00:00:00 2001 From: Boldi Date: Thu, 26 Feb 2026 18:16:17 +0000 Subject: [PATCH 10/19] Fixing line alignment, sub_circle colour and size. --- zxlive/proof.py | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/zxlive/proof.py b/zxlive/proof.py index c0969147..9d826bd2 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -598,7 +598,7 @@ def _open_sub_step_editor(self, step_idx: int, sub_idx: int) -> None: header_height = row_height sub_step_top = rect.y() + header_height + sub_idx * row_height - sub_text_x = int(sub_tree_x + delegate.sub_circle_radius + 10) + sub_text_x = int(sub_tree_x + delegate.circle_radius + 10) editor_x = sub_text_x # Center vertically in the row @@ -718,7 +718,6 @@ class ProofStepItemDelegate(QStyledItemDelegate): triangle_size = 5 sub_indent = 20 sub_branch_len = 15 - sub_circle_radius = 3 # Track hover position for sub-steps hover_step_idx: int = -1 @@ -937,7 +936,7 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, # Line down to last sub-step path.lineTo(sub_tree_x, last_sub_cy) # Line back to main axis at the bottom - path.lineTo(main_cx, bottom_y) + path.lineTo(main_cx - 0.3, bottom_y) painter.drawPath(path) @@ -958,7 +957,7 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, if is_sub_selected or is_sub_hovered: painter.setPen(Qt.GlobalColor.transparent) painter.setBrush(self._bg_color(is_sub_selected, False, is_sub_hovered)) - hl_left = int(sub_tree_x + self.sub_circle_radius + 2) + hl_left = int(sub_tree_x + self.circle_radius + 2) painter.drawRect(QRect( hl_left, int(sub_cy - row_height / 2), int(option.rect.width() - hl_left), row_height)) # type: ignore[attr-defined] @@ -966,17 +965,15 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, # Sub-step circle painter.setPen(QPen(line_clr, self.line_width)) if is_sub_selected: - painter.setBrush(QColor(30, 100, 200)) # brighter blue when selected - r = self.sub_circle_radius + 1 + painter.setBrush(display_setting.effective_colors["z_spider"]) # brighter blue when selected + r = self.circle_radius_selected else: - painter.setBrush(QColor(70, 130, 180)) # default steel-blue - r = self.sub_circle_radius - painter.drawEllipse( - QPointF(sub_tree_x, sub_cy), r, r - ) + painter.setBrush(display_setting.effective_colors["z_spider"]) # default steel-blue + r = self.circle_radius + painter.drawEllipse(QPointF(sub_tree_x, sub_cy), r, r) # Sub-step text - sub_text_x = int(sub_tree_x + self.sub_circle_radius + 10) + sub_text_x = int(sub_tree_x + self.circle_radius + 10) sub_text_rect = QRect( sub_text_x, int(sub_cy - text_height / 2), From 541f9e40477545e407aa5eb5e454d9c093f0bf20 Mon Sep 17 00:00:00 2001 From: axif Date: Fri, 27 Feb 2026 02:46:00 +0600 Subject: [PATCH 11/19] sub-step selection bugs and modernize type hints --- zxlive/commands.py | 42 +++++++++++++-------------- zxlive/proof.py | 72 +++++++++++++++++++++++++++++----------------- 2 files changed, 66 insertions(+), 48 deletions(-) diff --git a/zxlive/commands.py b/zxlive/commands.py index d08362e6..f52ff43c 100644 --- a/zxlive/commands.py +++ b/zxlive/commands.py @@ -4,7 +4,7 @@ from collections import namedtuple from dataclasses import dataclass, field from fractions import Fraction -from typing import Callable, Iterable, Optional, Set, Union +from typing import Callable, Iterable from PySide6.QtCore import QModelIndex from PySide6.QtGui import QUndoCommand @@ -104,7 +104,7 @@ def redo(self) -> None: class SetGraph(BaseCommand): """Replaces the current graph with an entirely new graph.""" new_g: GraphT - old_g: Optional[GraphT] = field(default=None, init=False) + old_g: GraphT | None = field(default=None, init=False) def undo(self) -> None: assert self.old_g is not None @@ -120,8 +120,8 @@ class UpdateGraph(BaseCommand): """Updates the current graph with a modified one. It will try to reuse existing QGraphicsItem's as much as possible.""" new_g: GraphT - old_g: Optional[GraphT] = field(default=None, init=False) - old_selected: Optional[Set[VT]] = field(default=None, init=False) + old_g: GraphT | None = field(default=None, init=False) + old_selected: set[VT] | None = field(default=None, init=False) def undo(self) -> None: assert self.old_g is not None and self.old_selected is not None @@ -145,9 +145,9 @@ class ChangeNodeType(BaseCommand): WInfo = namedtuple('WInfo', ['partner', 'partner_type', 'partner_pos', 'neighbors']) - _old_vtys: Optional[list[VertexType]] = field(default=None, init=False) - _old_w_info: Optional[dict[VT, WInfo]] = field(default=None, init=False) - _new_w_inputs: Optional[list[VT]] = field(default=None, init=False) + _old_vtys: list[VertexType] | None = field(default=None, init=False) + _old_w_info: dict[VT, WInfo] | None = field(default=None, init=False) + _new_w_inputs: list[VT] | None = field(default=None, init=False) def undo(self) -> None: assert self._old_vtys is not None @@ -212,7 +212,7 @@ class ChangeEdgeColor(BaseCommand): es: Iterable[ET] ety: EdgeType - _old_etys: Optional[list[EdgeType]] = field(default=None, init=False) + _old_etys: list[EdgeType] | None = field(default=None, init=False) def undo(self) -> None: assert self._old_etys is not None @@ -234,7 +234,7 @@ class AddNode(BaseCommand): y: float vty: VertexType - _added_vert: Optional[VT] = field(default=None, init=False) + _added_vert: VT | None = field(default=None, init=False) def undo(self) -> None: assert self._added_vert is not None @@ -256,10 +256,10 @@ class AddNodeSnapped(BaseCommand): vty: VertexType e: ET - added_vert: Optional[VT] = field(default=None, init=False) - s: Optional[VT] = field(default=None, init=False) - t: Optional[VT] = field(default=None, init=False) - _et: Optional[EdgeType] = field(default=None, init=False) + added_vert: VT | None = field(default=None, init=False) + s: VT | None = field(default=None, init=False) + t: VT | None = field(default=None, init=False) + _et: EdgeType | None = field(default=None, init=False) def undo(self) -> None: assert self.added_vert is not None @@ -297,8 +297,8 @@ class AddWNode(BaseCommand): x: float y: float - _added_input_vert: Optional[VT] = field(default=None, init=False) - _added_output_vert: Optional[VT] = field(default=None, init=False) + _added_input_vert: VT | None = field(default=None, init=False) + _added_output_vert: VT | None = field(default=None, init=False) def undo(self) -> None: assert self._added_input_vert is not None @@ -354,7 +354,7 @@ class MoveNode(BaseCommand): """Updates the location of a collection of nodes.""" vs: list[tuple[VT, float, float]] - _old_positions: Optional[list[tuple[float, float]]] = field(default=None, init=False) + _old_positions: list[tuple[float, float]] | None = field(default=None, init=False) def undo(self) -> None: assert self._old_positions is not None @@ -397,7 +397,7 @@ class MergeNodes(BaseCommand): """Merges groups of vertices that are at the same position.""" vertices_to_merge: list[VT] - _old_g: Optional[GraphT] = field(default=None, init=False) + _old_g: GraphT | None = field(default=None, init=False) def undo(self) -> None: assert self._old_g is not None @@ -431,9 +431,9 @@ def redo(self) -> None: class ChangePhase(BaseCommand): """Updates the phase of a spider.""" v: VT - new_phase: Union[Fraction, Poly, complex] + new_phase: Fraction | Poly | complex - _old_phase: Optional[Union[Fraction, Poly, complex]] = field(default=None, init=False) + _old_phase: Fraction | Poly | complex | None = field(default=None, init=False) def undo(self) -> None: assert self._old_phase is not None @@ -462,9 +462,9 @@ class AddRewriteStep(UpdateGraph): """ step_view: QListView name: str - diff: Optional[GraphDiff] = None + diff: GraphDiff | None = None - _old_selected: Optional[int] = field(default=None, init=False) + _old_selected: int | None = field(default=None, init=False) _old_steps: list[tuple[Rewrite, GraphT]] = field(default_factory=list, init=False) @property diff --git a/zxlive/proof.py b/zxlive/proof.py index 9d826bd2..7aef97b7 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -1,5 +1,7 @@ +from __future__ import annotations + import json -from typing import TYPE_CHECKING, Any, NamedTuple, Optional, Union, Dict +from typing import TYPE_CHECKING, Any, NamedTuple if TYPE_CHECKING: from .proof_panel import ProofPanel @@ -22,9 +24,9 @@ class Rewrite(NamedTuple): display_name: str # Name of proof displayed to user rule: str # Name of the rule that was applied to get to this step graph: GraphT # New graph after applying the rewrite - grouped_rewrites: Optional[list['Rewrite']] = None # Optional field to store the grouped rewrites + grouped_rewrites: list[Rewrite] | None = None # Optional field to store the grouped rewrites - def to_dict(self) -> Dict[str, Any]: + def to_dict(self) -> dict[str, Any]: """Serializes the rewrite to Python dictionary.""" return { "display_name": self.display_name, @@ -38,7 +40,7 @@ def to_json(self) -> str: return json.dumps(self.to_dict()) @staticmethod - def from_json(json_str: Union[str, Dict[str, Any]]) -> "Rewrite": + def from_json(json_str: str | dict[str, Any]) -> Rewrite: """Deserializes the rewrite from JSON or Python dict.""" if isinstance(json_str, str): d = json.loads(json_str) @@ -105,7 +107,7 @@ def set_sub_graph(self, step_idx: int, sub_idx: int, graph: GraphT) -> None: def graphs(self) -> list[GraphT]: return [self.initial_graph] + [step.graph for step in self.steps] - def data(self, index: Union[QModelIndex, QPersistentModelIndex], role: int = Qt.ItemDataRole.DisplayRole) -> Any: + def data(self, index: QModelIndex | QPersistentModelIndex, role: int = Qt.ItemDataRole.DisplayRole) -> Any: """Overrides `QAbstractItemModel.data` to populate a view with rewrite steps""" if index.row() >= len(self.steps) + 1 or index.column() >= 1: @@ -119,7 +121,7 @@ def data(self, index: Union[QModelIndex, QPersistentModelIndex], role: int = Qt. elif role == Qt.ItemDataRole.FontRole: return QFont("monospace", 12) - def flags(self, index: Union[QModelIndex, QPersistentModelIndex]) -> Qt.ItemFlag: + def flags(self, index: QModelIndex | QPersistentModelIndex) -> Qt.ItemFlag: if index.row() == 0: return super().flags(index) return super().flags(index) | Qt.ItemFlag.ItemIsEditable @@ -132,11 +134,11 @@ def headerData(self, section: int, orientation: Qt.Orientation, """ return None - def columnCount(self, index: Union[QModelIndex, QPersistentModelIndex] = QModelIndex()) -> int: + def columnCount(self, index: QModelIndex | QPersistentModelIndex = QModelIndex()) -> int: """The number of columns""" return 1 - def rowCount(self, index: Union[QModelIndex, QPersistentModelIndex] = QModelIndex()) -> int: + def rowCount(self, index: 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 @@ -146,7 +148,7 @@ def rowCount(self, index: Union[QModelIndex, QPersistentModelIndex] = QModelInde else: return 0 - def add_rewrite(self, rewrite: Rewrite, position: Optional[int] = None) -> None: + def add_rewrite(self, rewrite: Rewrite, position: int | None = None) -> None: """Adds a rewrite step to the model.""" if position is None: position = len(self.steps) @@ -154,7 +156,7 @@ def add_rewrite(self, rewrite: Rewrite, position: Optional[int] = None) -> None: self.steps.insert(position, rewrite) self.endInsertRows() - def pop_rewrite(self, position: Optional[int] = None) -> tuple[Rewrite, GraphT]: + def pop_rewrite(self, position: int | None = None) -> tuple[Rewrite, GraphT]: """Removes the latest rewrite from the model. Returns the rewrite and the graph that previously resulted from this rewrite. @@ -250,7 +252,7 @@ def ungroup_steps(self, index: int) -> None: self.createIndex(index + len(individual_steps), 0), []) - def to_dict(self) -> Dict[str, Any]: + def to_dict(self) -> dict[str, Any]: """Serializes the model to Python dict.""" initial_graph = self.initial_graph.to_dict() proof_steps = [step.to_dict() for step in self.steps] @@ -265,7 +267,7 @@ def to_json(self) -> str: return json.dumps(self.to_dict()) @staticmethod - def from_json(json_str: Union[str, Dict[str, Any]]) -> "ProofModel": + def from_json(json_str: str | dict[str, Any]) -> ProofModel: """Deserializes the model from JSON or Python dict.""" if isinstance(json_str, str): d = json.loads(json_str) @@ -286,14 +288,14 @@ def from_json(json_str: Union[str, Dict[str, Any]]) -> "ProofModel": class ProofStepView(QListView): """A view for displaying the steps in a proof.""" - def __init__(self, parent: 'ProofPanel'): + def __init__(self, parent: ProofPanel): super().__init__(parent) self.graph_view = parent.graph_view self.undo_stack = parent.undo_stack self.expanded_groups: set[int] = set() # Track currently selected sub-step: (step_index, sub_step_index) or None - self.selected_sub_step: Optional[tuple[int, int]] = None - self._active_sub_editor: Optional[QLineEdit] = 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) @@ -413,6 +415,10 @@ def mousePressEvent(self, event: QMouseEvent) -> None: # type: ignore[override] index = self.indexAt(event.pos()) toggle_idx = -1 sub_step_clicked = False + # Save old sub-step selection; if the user clicks a sub-step in a + # different group we need to repaint the old group's row to clear + # its stale highlight. + old_sub_step = self.selected_sub_step if index.isValid() and index.row() > 0: step_idx = index.row() - 1 @@ -443,7 +449,20 @@ def mousePressEvent(self, event: QMouseEvent) -> None: # type: ignore[override] old_model_idx = self.model().index(old_step_idx + 1, 0) self.model().dataChanged.emit(old_model_idx, old_model_idx, []) - super().mousePressEvent(event) + if sub_step_clicked: + # Repaint the old group's row if we switched from a different group, + # so the stale sub-step highlight is cleared. + if old_sub_step is not None and old_sub_step[0] != step_idx: + old_model_idx = self.model().index(old_sub_step[0] + 1, 0) + self.model().dataChanged.emit(old_model_idx, old_model_idx, []) + # Select the parent row in QListView so it appears as the active + # step, but block signals to prevent proof_step_selected from + # overwriting the sub-step graph we just navigated to. + self.selectionModel().blockSignals(True) + self.setCurrentIndex(index) + self.selectionModel().blockSignals(False) + else: + super().mousePressEvent(event) if toggle_idx >= 0: self.toggle_group_expansion(toggle_idx) @@ -725,7 +744,7 @@ class ProofStepItemDelegate(QStyledItemDelegate): # Track hover over group header hover_header_step_idx: int = -1 - def _step_info(self, index: Union[QModelIndex, QPersistentModelIndex]) -> tuple[bool, bool, Optional[list['Rewrite']]]: + def _step_info(self, index: QModelIndex | QPersistentModelIndex) -> tuple[bool, bool, list[Rewrite] | None]: """Return (is_grouped, is_expanded, grouped_rewrites) for a given row.""" if index.row() == 0: return False, False, None @@ -761,7 +780,7 @@ def _bg_color(selected: bool, sub_selected: bool, hovered: bool) -> QColor: return QColor(229, 243, 255) return QColor(255, 255, 255) - def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> None: + def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: QModelIndex | QPersistentModelIndex) -> None: painter.save() painter.setRenderHint(QPainter.RenderHint.Antialiasing) @@ -910,7 +929,7 @@ def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QM def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, step_idx: int, - grouped_rewrites: list['Rewrite'], row_height: int, + grouped_rewrites: list[Rewrite], row_height: int, text_height: int, font: QFont, fg: QColor, line_clr: QColor) -> None: main_cx = self.line_padding + self.line_width / 2 @@ -953,14 +972,13 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, # Check if this sub-step is being hovered (for individual hover effect) is_sub_hovered = (self.hover_step_idx == step_idx and self.hover_sub_idx == i) - # Highlight starts AFTER the branch line (matching ungrouped style) + # Highlight spans the full width of the item, starting from the left edge if is_sub_selected or is_sub_hovered: painter.setPen(Qt.GlobalColor.transparent) painter.setBrush(self._bg_color(is_sub_selected, False, is_sub_hovered)) - hl_left = int(sub_tree_x + self.circle_radius + 2) painter.drawRect(QRect( - hl_left, int(sub_cy - row_height / 2), - int(option.rect.width() - hl_left), row_height)) # type: ignore[attr-defined] + option.rect.x(), int(sub_cy - row_height / 2), # type: ignore[attr-defined] + option.rect.width(), row_height)) # type: ignore[attr-defined] # Sub-step circle painter.setPen(QPen(line_clr, self.line_width)) @@ -987,7 +1005,7 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, painter.setPen(fg) painter.drawText(sub_text_rect, Qt.AlignmentFlag.AlignLeft, sub_step.display_name) - def sizeHint(self, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> QSize: + def sizeHint(self, option: QStyleOptionViewItem, index: QModelIndex | QPersistentModelIndex) -> QSize: size = super().sizeHint(option, index) text_height = QFontMetrics(option.font).height() # type: ignore[attr-defined] single_row = text_height + 2 * self.vert_padding @@ -999,15 +1017,15 @@ def sizeHint(self, option: QStyleOptionViewItem, index: Union[QModelIndex, QPers return QSize(size.width(), total) - def createEditor(self, parent: QWidget, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> QLineEdit: + def createEditor(self, parent: QWidget, option: QStyleOptionViewItem, index: QModelIndex | QPersistentModelIndex) -> QLineEdit: return QLineEdit(parent) - def setEditorData(self, editor: QWidget, index: Union[QModelIndex, QPersistentModelIndex]) -> None: + def setEditorData(self, editor: QWidget, index: QModelIndex | QPersistentModelIndex) -> None: assert isinstance(editor, QLineEdit) value = index.model().data(index, Qt.ItemDataRole.DisplayRole) editor.setText(str(value)) - def setModelData(self, editor: QWidget, model: QAbstractItemModel, index: Union[QModelIndex, QPersistentModelIndex]) -> None: + def setModelData(self, editor: QWidget, model: QAbstractItemModel, index: QModelIndex | QPersistentModelIndex) -> None: step_view = self.parent() assert isinstance(step_view, ProofStepView) assert isinstance(editor, QLineEdit) From 3581d2ebd569332225deb92f253414dbea2468ae Mon Sep 17 00:00:00 2001 From: axif Date: Fri, 27 Feb 2026 03:42:54 +0600 Subject: [PATCH 12/19] refactor: Reorder sub-step drawing in `ProofStepDelegate` to ensure highlights are rendered in the background. --- zxlive/proof.py | 37 ++++++++++++++++++++++++------------- 1 file changed, 24 insertions(+), 13 deletions(-) diff --git a/zxlive/proof.py b/zxlive/proof.py index 7aef97b7..6531b67a 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -941,12 +941,34 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, last_sub_cy = option.rect.y() + row_height + (n - 1) * row_height + row_height / 2 # type: ignore[attr-defined] bottom_y = option.rect.y() + option.rect.height() # type: ignore[attr-defined] + # 1. Draw sub-step highlights first so they sit in the background + for i, sub_step in enumerate(grouped_rewrites): + sub_cy = first_sub_cy + i * row_height + is_sub_selected = False + # Determine which sub-step is selected (if any) + view = self.parent() + if isinstance(view, ProofStepView) and view.selected_sub_step is not None: + sel_step_idx, sel_sub_idx = view.selected_sub_step + if step_idx == sel_step_idx and i == sel_sub_idx: + is_sub_selected = True + + # Check if this sub-step is being hovered (for individual hover effect) + is_sub_hovered = (self.hover_step_idx == step_idx and self.hover_sub_idx == i) + + # Highlight spans the full width of the item, starting from the left edge + if is_sub_selected or is_sub_hovered: + painter.setPen(Qt.GlobalColor.transparent) + painter.setBrush(self._bg_color(is_sub_selected, False, is_sub_hovered)) + painter.drawRect(QRect( + option.rect.x(), int(sub_cy - row_height / 2), # type: ignore[attr-defined] + option.rect.width(), row_height)) # type: ignore[attr-defined] + + # 2. Draw the path connecting header -> sub-steps -> next step pen = QPen(line_clr, self.line_width) pen.setCapStyle(Qt.PenCapStyle.RoundCap) painter.setPen(pen) painter.setBrush(Qt.GlobalColor.transparent) - # Path connecting header -> sub-steps -> next step path = QPainterPath() # Start at the headers circle path.moveTo(main_cx, header_cy) @@ -959,27 +981,16 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, painter.drawPath(path) + # 3. Draw sub-step circles and text for i, sub_step in enumerate(grouped_rewrites): sub_cy = first_sub_cy + i * row_height is_sub_selected = False - # Determine which sub-step is selected (if any) view = self.parent() if isinstance(view, ProofStepView) and view.selected_sub_step is not None: sel_step_idx, sel_sub_idx = view.selected_sub_step if step_idx == sel_step_idx and i == sel_sub_idx: is_sub_selected = True - # Check if this sub-step is being hovered (for individual hover effect) - is_sub_hovered = (self.hover_step_idx == step_idx and self.hover_sub_idx == i) - - # Highlight spans the full width of the item, starting from the left edge - if is_sub_selected or is_sub_hovered: - painter.setPen(Qt.GlobalColor.transparent) - painter.setBrush(self._bg_color(is_sub_selected, False, is_sub_hovered)) - painter.drawRect(QRect( - option.rect.x(), int(sub_cy - row_height / 2), # type: ignore[attr-defined] - option.rect.width(), row_height)) # type: ignore[attr-defined] - # Sub-step circle painter.setPen(QPen(line_clr, self.line_width)) if is_sub_selected: From 693c806144b7311022d49724afee81bc0fcddac9 Mon Sep 17 00:00:00 2001 From: axif Date: Sat, 28 Feb 2026 04:16:33 +0600 Subject: [PATCH 13/19] feat: Implement rewriting from within a grouped sub-step, including truncation and ungrouping, with corresponding undo functionality. --- zxlive/commands.py | 78 +++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 71 insertions(+), 7 deletions(-) diff --git a/zxlive/commands.py b/zxlive/commands.py index f52ff43c..c26f60b9 100644 --- a/zxlive/commands.py +++ b/zxlive/commands.py @@ -466,6 +466,11 @@ class AddRewriteStep(UpdateGraph): _old_selected: int | None = field(default=None, init=False) _old_steps: list[tuple[Rewrite, GraphT]] = field(default_factory=list, init=False) + # 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) @property def proof_model(self) -> ProofModel: @@ -474,15 +479,62 @@ def proof_model(self) -> ProofModel: return model def redo(self) -> None: - # Remove steps from the proof model until we're at the currently selected step self._old_selected = int(self.step_view.currentIndex().row()) self._old_steps = [] - for _ in range(self.proof_model.rowCount() - self._old_selected - 1): - self._old_steps.append(self.proof_model.pop_rewrite()) + self._old_group_tail = None + self._old_group_rewrite = None + + # Check whether the user is rewriting from inside a grouped sub-step. + step_view = self.step_view + sub_step: tuple[int, int] | None = ( + step_view.selected_sub_step # type: ignore[union-attr] + if isinstance(step_view, ProofStepView) else None + ) + + if sub_step is not None: + group_step_idx, sub_idx = sub_step # 0-based indices into proof_model.steps + + # 1. Pop all main steps that come AFTER the grouped step (rightmost first). + steps_after_group = self.proof_model.rowCount() - 1 - (group_step_idx + 1) + for _ in range(steps_after_group): + self._old_steps.append(self.proof_model.pop_rewrite()) + + # 2. Truncate the grouped step: keep only sub-steps 0..sub_idx (inclusive). + old_group = self.proof_model.steps[group_step_idx] + assert old_group.grouped_rewrites is not None + self._old_group_rewrite = old_group + + kept = old_group.grouped_rewrites[:sub_idx + 1] + self._old_group_tail = old_group.grouped_rewrites[sub_idx + 1:] + + if len(kept) == 1: + # Ungroup: replace the grouped step with the single sub-step. + self.proof_model.pop_rewrite(group_step_idx) + self.proof_model.add_rewrite(kept[0], group_step_idx) + else: + # Update the group in-place with the truncated sub-steps. + new_group = Rewrite( + old_group.display_name, + old_group.rule, + kept[-1].graph, + kept, + ) + self.proof_model.steps[group_step_idx] = new_group + model_index = self.proof_model.createIndex(group_step_idx + 1, 0) + self.proof_model.dataChanged.emit(model_index, model_index, []) + + # Clear the sub-step selection since we are moving outside the group. + if isinstance(step_view, ProofStepView): + step_view.selected_sub_step = None + + else: + # Normal case: remove all steps after the currently selected step. + for _ in range(self.proof_model.rowCount() - self._old_selected - 1): + self._old_steps.append(self.proof_model.pop_rewrite()) self.proof_model.add_rewrite(Rewrite(self.name, self.name, self.new_g)) - # Select the added step + # Select the added step. idx = self.step_view.model().index(self.proof_model.rowCount() - 1, 0, QModelIndex()) self.step_view.selectionModel().blockSignals(True) self.step_view.setCurrentIndex(idx) @@ -490,16 +542,28 @@ def redo(self) -> None: super().redo() def undo(self) -> None: - # Undo the rewrite + # Remove the newly added rewrite. self.step_view.selectionModel().blockSignals(True) self.proof_model.pop_rewrite() self.step_view.selectionModel().blockSignals(False) - # Add back steps that were previously removed + if self._old_group_rewrite is not None: + # We had truncated (and possibly ungrouped) a group step. + # The group is at group_step_idx == _old_selected - 1. + assert self._old_selected is not None + group_step_idx = self._old_selected - 1 + + # Remove the current (truncated/ungrouped) step at that position. + self.proof_model.pop_rewrite(group_step_idx) + + # Restore the original grouped step. + self.proof_model.add_rewrite(self._old_group_rewrite, group_step_idx) + + # Restore main steps after the group (they were popped LIFO, restore in reverse). for rewrite, graph in reversed(self._old_steps): self.proof_model.add_rewrite(rewrite) - # Select the previously selected step + # Restore the previously selected step. assert self._old_selected is not None idx = self.step_view.model().index(self._old_selected, 0, QModelIndex()) self.step_view.selectionModel().blockSignals(True) From b8d129e75785a794576b18a16705f60c22c78ebd Mon Sep 17 00:00:00 2001 From: axif Date: Sat, 28 Feb 2026 20:26:58 +0600 Subject: [PATCH 14/19] extract click and hover target detection logic into dedicated helper methods for improved readability. --- zxlive/proof.py | 100 ++++++++++++++++++++++++++---------------------- 1 file changed, 55 insertions(+), 45 deletions(-) diff --git a/zxlive/proof.py b/zxlive/proof.py index 6531b67a..f545c219 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -406,6 +406,37 @@ def _navigate_to_sub_step(self, step_idx: int, sub_idx: int) -> None: model_index = self.model().index(step_idx + 1, 0) self.model().dataChanged.emit(model_index, model_index, []) + def _click_target_for_pos(self, event: QMouseEvent) -> tuple[int, bool, int]: + """Classify a mouse-press into (toggle_idx, sub_step_clicked, step_idx). + + toggle_idx – step index whose triangle was clicked, or -1 + sub_step_clicked – True when a sub-step row was clicked + step_idx – the step row the click landed on (only meaningful + when toggle_idx >= 0 or sub_step_clicked is True) + """ + index = self.indexAt(event.pos()) + if not index.isValid() or index.row() <= 0: + return -1, False, -1 + step_idx = index.row() - 1 + if step_idx >= len(self.model().steps): + return -1, False, -1 + step = self.model().steps[step_idx] + if step.grouped_rewrites is None: + return -1, False, -1 + delegate = self.itemDelegate() + if not isinstance(delegate, ProofStepItemDelegate): + return -1, False, -1 + rect = self.visualRect(index) + if self._triangle_hit_test(step_idx, int(event.pos().x()), int(event.pos().y()), + rect.x(), rect.y()): + return step_idx, False, step_idx # triangle clicked → toggle + if step_idx in self.expanded_groups: + sub_idx = self._sub_step_hit_test(step_idx, int(event.pos().y()), rect.y()) + if sub_idx >= 0: + self._navigate_to_sub_step(step_idx, sub_idx) + return -1, True, step_idx # sub-step clicked + return -1, False, -1 + def mousePressEvent(self, event: QMouseEvent) -> None: # type: ignore[override] """Handle mouse clicks on grouped steps to toggle expansion. @@ -413,34 +444,12 @@ def mousePressEvent(self, event: QMouseEvent) -> None: # type: ignore[override] Clicking on a sub-step navigates to that sub-step's graph. """ index = self.indexAt(event.pos()) - toggle_idx = -1 - sub_step_clicked = False # Save old sub-step selection; if the user clicks a sub-step in a # different group we need to repaint the old group's row to clear # its stale highlight. old_sub_step = self.selected_sub_step - 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()), - rect.x(), rect.y()): - toggle_idx = step_idx - elif step_idx in self.expanded_groups: - # Expanded: check if clicking on a sub-step - sub_idx = self._sub_step_hit_test( - step_idx, int(event.pos().y()), rect.y() - ) - if sub_idx >= 0: - # Clicked on a sub-step - sub_step_clicked = True - self._navigate_to_sub_step(step_idx, sub_idx) + toggle_idx, sub_step_clicked, step_idx = self._click_target_for_pos(event) # Clear sub-step selection when clicking on a non-sub-step area if not sub_step_clicked and self.selected_sub_step is not None: @@ -471,6 +480,28 @@ def _repaint_step(self, step_idx: int) -> None: """Trigger repaint for a step row by its 0-based step index.""" self.update(self.model().index(step_idx + 1, 0)) + def _hover_target_for_pos(self, pos: Any) -> tuple[int, int, int]: + """Return (new_step, new_sub, new_header) for the given mouse position. + + Each value is -1 when not applicable. + """ + index = self.indexAt(pos) + if not index.isValid() or index.row() <= 0: + return -1, -1, -1 + step_idx = index.row() - 1 + if step_idx >= len(self.model().steps): + return -1, -1, -1 + step = self.model().steps[step_idx] + if step.grouped_rewrites is None: + return -1, -1, -1 + if step_idx not in self.expanded_groups: + return -1, -1, step_idx + rect = self.visualRect(index) + sub_idx = self._sub_step_hit_test(step_idx, int(pos.y()), rect.y()) + if sub_idx >= 0: + return step_idx, sub_idx, -1 + return -1, -1, step_idx + def mouseMoveEvent(self, event: QMouseEvent) -> None: # type: ignore[override] """Track which sub-step the mouse is hovering over and trigger repaint.""" delegate = self.itemDelegate() @@ -481,28 +512,7 @@ def mouseMoveEvent(self, event: QMouseEvent) -> None: # type: ignore[override] old_step = delegate.hover_step_idx old_sub = delegate.hover_sub_idx old_header = delegate.hover_header_step_idx - new_step = -1 - new_sub = -1 - new_header = -1 - - index = self.indexAt(event.pos()) - 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 - new_sub = sub_idx - else: - new_header = step_idx - else: - new_header = step_idx + new_step, new_sub, new_header = self._hover_target_for_pos(event.pos()) if new_step != old_step or new_sub != old_sub: delegate.hover_step_idx = new_step From 0a51d6fabff01c171afe5e392236d3c1e3bf64f4 Mon Sep 17 00:00:00 2001 From: axif Date: Mon, 2 Mar 2026 03:10:27 +0600 Subject: [PATCH 15/19] undo type hint changes of mine --- zxlive/commands.py | 58 +++++++++++++++++++++++----------------------- zxlive/proof.py | 54 +++++++++++++++++++++--------------------- 2 files changed, 56 insertions(+), 56 deletions(-) diff --git a/zxlive/commands.py b/zxlive/commands.py index c26f60b9..68098fef 100644 --- a/zxlive/commands.py +++ b/zxlive/commands.py @@ -4,7 +4,7 @@ from collections import namedtuple from dataclasses import dataclass, field from fractions import Fraction -from typing import Callable, Iterable +from typing import Callable, Iterable, Optional, Set, Union, List, Dict, Tuple from PySide6.QtCore import QModelIndex from PySide6.QtGui import QUndoCommand @@ -104,7 +104,7 @@ def redo(self) -> None: class SetGraph(BaseCommand): """Replaces the current graph with an entirely new graph.""" new_g: GraphT - old_g: GraphT | None = field(default=None, init=False) + old_g: Optional[GraphT] = field(default=None, init=False) def undo(self) -> None: assert self.old_g is not None @@ -120,8 +120,8 @@ class UpdateGraph(BaseCommand): """Updates the current graph with a modified one. It will try to reuse existing QGraphicsItem's as much as possible.""" new_g: GraphT - old_g: GraphT | None = field(default=None, init=False) - old_selected: set[VT] | None = field(default=None, init=False) + old_g: Optional[GraphT] = field(default=None, init=False) + old_selected: Optional[Set[VT]] = field(default=None, init=False) def undo(self) -> None: assert self.old_g is not None and self.old_selected is not None @@ -140,14 +140,14 @@ def redo(self) -> None: @dataclass class ChangeNodeType(BaseCommand): """Changes the color of a set of spiders.""" - vs: list[VT] | set[VT] + vs: Union[List[VT], Set[VT]] vty: VertexType WInfo = namedtuple('WInfo', ['partner', 'partner_type', 'partner_pos', 'neighbors']) - _old_vtys: list[VertexType] | None = field(default=None, init=False) - _old_w_info: dict[VT, WInfo] | None = field(default=None, init=False) - _new_w_inputs: list[VT] | None = field(default=None, init=False) + _old_vtys: Optional[List[VertexType]] = field(default=None, init=False) + _old_w_info: Optional[Dict[VT, WInfo]] = field(default=None, init=False) + _new_w_inputs: Optional[List[VT]] = field(default=None, init=False) def undo(self) -> None: assert self._old_vtys is not None @@ -212,7 +212,7 @@ class ChangeEdgeColor(BaseCommand): es: Iterable[ET] ety: EdgeType - _old_etys: list[EdgeType] | None = field(default=None, init=False) + _old_etys: Optional[List[EdgeType]] = field(default=None, init=False) def undo(self) -> None: assert self._old_etys is not None @@ -234,7 +234,7 @@ class AddNode(BaseCommand): y: float vty: VertexType - _added_vert: VT | None = field(default=None, init=False) + _added_vert: Optional[VT] = field(default=None, init=False) def undo(self) -> None: assert self._added_vert is not None @@ -256,10 +256,10 @@ class AddNodeSnapped(BaseCommand): vty: VertexType e: ET - added_vert: VT | None = field(default=None, init=False) - s: VT | None = field(default=None, init=False) - t: VT | None = field(default=None, init=False) - _et: EdgeType | None = field(default=None, init=False) + added_vert: Optional[VT] = field(default=None, init=False) + s: Optional[VT] = field(default=None, init=False) + t: Optional[VT] = field(default=None, init=False) + _et: Optional[EdgeType] = field(default=None, init=False) def undo(self) -> None: assert self.added_vert is not None @@ -297,8 +297,8 @@ class AddWNode(BaseCommand): x: float y: float - _added_input_vert: VT | None = field(default=None, init=False) - _added_output_vert: VT | None = field(default=None, init=False) + _added_input_vert: Optional[VT] = field(default=None, init=False) + _added_output_vert: Optional[VT] = field(default=None, init=False) def undo(self) -> None: assert self._added_input_vert is not None @@ -335,7 +335,7 @@ def redo(self) -> None: @dataclass class AddEdges(BaseCommand): """Adds multiple edges of the same type to a graph.""" - pairs: list[tuple[VT, VT]] + pairs: List[Tuple[VT, VT]] ety: EdgeType def undo(self) -> None: @@ -352,9 +352,9 @@ def redo(self) -> None: @dataclass class MoveNode(BaseCommand): """Updates the location of a collection of nodes.""" - vs: list[tuple[VT, float, float]] + vs: List[Tuple[VT, float, float]] - _old_positions: list[tuple[float, float]] | None = field(default=None, init=False) + _old_positions: Optional[List[Tuple[float, float]]] = field(default=None, init=False) def undo(self) -> None: assert self._old_positions is not None @@ -395,9 +395,9 @@ def redo(self) -> None: @dataclass class MergeNodes(BaseCommand): """Merges groups of vertices that are at the same position.""" - vertices_to_merge: list[VT] + vertices_to_merge: List[VT] - _old_g: GraphT | None = field(default=None, init=False) + _old_g: Optional[GraphT] = field(default=None, init=False) def undo(self) -> None: assert self._old_g is not None @@ -431,9 +431,9 @@ def redo(self) -> None: class ChangePhase(BaseCommand): """Updates the phase of a spider.""" v: VT - new_phase: Fraction | Poly | complex + new_phase: Union[Fraction, Poly, complex] - _old_phase: Fraction | Poly | complex | None = field(default=None, init=False) + _old_phase: Optional[Union[Fraction, Poly, complex]] = field(default=None, init=False) def undo(self) -> None: assert self._old_phase is not None @@ -462,15 +462,15 @@ class AddRewriteStep(UpdateGraph): """ step_view: QListView name: str - diff: GraphDiff | None = None + diff: Optional[GraphDiff] = None - _old_selected: int | None = field(default=None, init=False) - _old_steps: list[tuple[Rewrite, GraphT]] = field(default_factory=list, init=False) + _old_selected: Optional[int] = field(default=None, init=False) + _old_steps: List[Tuple[Rewrite, GraphT]] = field(default_factory=list, init=False) # 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) + _old_group_tail: Optional[List[Rewrite]] = 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) + _old_group_rewrite: Optional[Rewrite] = field(default=None, init=False) @property def proof_model(self) -> ProofModel: @@ -486,7 +486,7 @@ def redo(self) -> None: # Check whether the user is rewriting from inside a grouped sub-step. step_view = self.step_view - sub_step: tuple[int, int] | None = ( + sub_step: Optional[Tuple[int, int]] = ( step_view.selected_sub_step # type: ignore[union-attr] if isinstance(step_view, ProofStepView) else None ) diff --git a/zxlive/proof.py b/zxlive/proof.py index f545c219..48c23b2c 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -1,7 +1,7 @@ from __future__ import annotations import json -from typing import TYPE_CHECKING, Any, NamedTuple +from typing import TYPE_CHECKING, Any, NamedTuple, Optional, Union, Dict, List, Tuple, Set if TYPE_CHECKING: from .proof_panel import ProofPanel @@ -24,9 +24,9 @@ class Rewrite(NamedTuple): display_name: str # Name of proof displayed to user rule: str # Name of the rule that was applied to get to this step graph: GraphT # New graph after applying the rewrite - grouped_rewrites: list[Rewrite] | None = None # Optional field to store the grouped rewrites + grouped_rewrites: Optional[List['Rewrite']] = None # Optional field to store the grouped rewrites - def to_dict(self) -> dict[str, Any]: + def to_dict(self) -> Dict[str, Any]: """Serializes the rewrite to Python dictionary.""" return { "display_name": self.display_name, @@ -40,7 +40,7 @@ def to_json(self) -> str: return json.dumps(self.to_dict()) @staticmethod - def from_json(json_str: str | dict[str, Any]) -> Rewrite: + def from_json(json_str: Union[str, Dict[str, Any]]) -> "Rewrite": """Deserializes the rewrite from JSON or Python dict.""" if isinstance(json_str, str): d = json.loads(json_str) @@ -67,7 +67,7 @@ class ProofModel(QAbstractListModel): """ initial_graph: GraphT - steps: list[Rewrite] + steps: List['Rewrite'] def __init__(self, start_graph: GraphT): super().__init__() @@ -104,10 +104,10 @@ def set_sub_graph(self, step_idx: int, sub_idx: int, graph: GraphT) -> None: modelIndex = self.createIndex(step_idx + 1, 0) self.dataChanged.emit(modelIndex, modelIndex, []) - def graphs(self) -> list[GraphT]: + def graphs(self) -> List[GraphT]: return [self.initial_graph] + [step.graph for step in self.steps] - def data(self, index: QModelIndex | QPersistentModelIndex, role: int = Qt.ItemDataRole.DisplayRole) -> Any: + def data(self, index: Union[QModelIndex, QPersistentModelIndex], role: int = Qt.ItemDataRole.DisplayRole) -> Any: """Overrides `QAbstractItemModel.data` to populate a view with rewrite steps""" if index.row() >= len(self.steps) + 1 or index.column() >= 1: @@ -121,7 +121,7 @@ def data(self, index: QModelIndex | QPersistentModelIndex, role: int = Qt.ItemDa elif role == Qt.ItemDataRole.FontRole: return QFont("monospace", 12) - def flags(self, index: QModelIndex | QPersistentModelIndex) -> Qt.ItemFlag: + def flags(self, index: Union[QModelIndex, QPersistentModelIndex]) -> Qt.ItemFlag: if index.row() == 0: return super().flags(index) return super().flags(index) | Qt.ItemFlag.ItemIsEditable @@ -134,11 +134,11 @@ def headerData(self, section: int, orientation: Qt.Orientation, """ return None - def columnCount(self, index: QModelIndex | QPersistentModelIndex = QModelIndex()) -> int: + def columnCount(self, index: Union[QModelIndex, QPersistentModelIndex] = QModelIndex()) -> int: """The number of columns""" return 1 - def rowCount(self, index: QModelIndex | QPersistentModelIndex = QModelIndex()) -> int: + def rowCount(self, index: 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 @@ -148,7 +148,7 @@ def rowCount(self, index: QModelIndex | QPersistentModelIndex = QModelIndex()) - else: return 0 - def add_rewrite(self, rewrite: Rewrite, position: int | None = None) -> None: + def add_rewrite(self, rewrite: Rewrite, position: Optional[int] = None) -> None: """Adds a rewrite step to the model.""" if position is None: position = len(self.steps) @@ -156,7 +156,7 @@ def add_rewrite(self, rewrite: Rewrite, position: int | None = None) -> None: self.steps.insert(position, rewrite) self.endInsertRows() - def pop_rewrite(self, position: int | None = None) -> tuple[Rewrite, GraphT]: + def pop_rewrite(self, position: Optional[int] = None) -> Tuple[Rewrite, GraphT]: """Removes the latest rewrite from the model. Returns the rewrite and the graph that previously resulted from this rewrite. @@ -252,7 +252,7 @@ def ungroup_steps(self, index: int) -> None: self.createIndex(index + len(individual_steps), 0), []) - def to_dict(self) -> dict[str, Any]: + def to_dict(self) -> Dict[str, Any]: """Serializes the model to Python dict.""" initial_graph = self.initial_graph.to_dict() proof_steps = [step.to_dict() for step in self.steps] @@ -267,7 +267,7 @@ def to_json(self) -> str: return json.dumps(self.to_dict()) @staticmethod - def from_json(json_str: str | dict[str, Any]) -> ProofModel: + def from_json(json_str: Union[str, Dict[str, Any]]) -> "ProofModel": """Deserializes the model from JSON or Python dict.""" if isinstance(json_str, str): d = json.loads(json_str) @@ -288,14 +288,14 @@ def from_json(json_str: str | dict[str, Any]) -> ProofModel: class ProofStepView(QListView): """A view for displaying the steps in a proof.""" - def __init__(self, parent: ProofPanel): + def __init__(self, parent: 'ProofPanel'): super().__init__(parent) self.graph_view = parent.graph_view self.undo_stack = parent.undo_stack - self.expanded_groups: set[int] = set() + 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.selected_sub_step: Optional[Tuple[int, int]] = None + self._active_sub_editor: Optional[QLineEdit] = None self.setModel(ProofModel(self.graph_view.graph_scene.g)) self.setCurrentIndex(self.model().index(0, 0)) self.setEditTriggers(QAbstractItemView.EditTrigger.DoubleClicked) @@ -406,7 +406,7 @@ def _navigate_to_sub_step(self, step_idx: int, sub_idx: int) -> None: model_index = self.model().index(step_idx + 1, 0) self.model().dataChanged.emit(model_index, model_index, []) - def _click_target_for_pos(self, event: QMouseEvent) -> tuple[int, bool, int]: + def _click_target_for_pos(self, event: QMouseEvent) -> Tuple[int, bool, int]: """Classify a mouse-press into (toggle_idx, sub_step_clicked, step_idx). toggle_idx – step index whose triangle was clicked, or -1 @@ -480,7 +480,7 @@ def _repaint_step(self, step_idx: int) -> None: """Trigger repaint for a step row by its 0-based step index.""" self.update(self.model().index(step_idx + 1, 0)) - def _hover_target_for_pos(self, pos: Any) -> tuple[int, int, int]: + def _hover_target_for_pos(self, pos: Any) -> Tuple[int, int, int]: """Return (new_step, new_sub, new_header) for the given mouse position. Each value is -1 when not applicable. @@ -754,7 +754,7 @@ class ProofStepItemDelegate(QStyledItemDelegate): # Track hover over group header hover_header_step_idx: int = -1 - def _step_info(self, index: QModelIndex | QPersistentModelIndex) -> tuple[bool, bool, list[Rewrite] | None]: + def _step_info(self, index: Union[QModelIndex, QPersistentModelIndex]) -> Tuple[bool, bool, Optional[List['Rewrite']]]: """Return (is_grouped, is_expanded, grouped_rewrites) for a given row.""" if index.row() == 0: return False, False, None @@ -790,7 +790,7 @@ def _bg_color(selected: bool, sub_selected: bool, hovered: bool) -> QColor: return QColor(229, 243, 255) return QColor(255, 255, 255) - def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: QModelIndex | QPersistentModelIndex) -> None: + def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> None: painter.save() painter.setRenderHint(QPainter.RenderHint.Antialiasing) @@ -939,7 +939,7 @@ def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: QModelIn def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, step_idx: int, - grouped_rewrites: list[Rewrite], row_height: int, + grouped_rewrites: List['Rewrite'], row_height: int, text_height: int, font: QFont, fg: QColor, line_clr: QColor) -> None: main_cx = self.line_padding + self.line_width / 2 @@ -1026,7 +1026,7 @@ def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, painter.setPen(fg) painter.drawText(sub_text_rect, Qt.AlignmentFlag.AlignLeft, sub_step.display_name) - def sizeHint(self, option: QStyleOptionViewItem, index: QModelIndex | QPersistentModelIndex) -> QSize: + def sizeHint(self, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> QSize: size = super().sizeHint(option, index) text_height = QFontMetrics(option.font).height() # type: ignore[attr-defined] single_row = text_height + 2 * self.vert_padding @@ -1038,15 +1038,15 @@ def sizeHint(self, option: QStyleOptionViewItem, index: QModelIndex | QPersisten return QSize(size.width(), total) - def createEditor(self, parent: QWidget, option: QStyleOptionViewItem, index: QModelIndex | QPersistentModelIndex) -> QLineEdit: + def createEditor(self, parent: QWidget, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> QLineEdit: return QLineEdit(parent) - def setEditorData(self, editor: QWidget, index: QModelIndex | QPersistentModelIndex) -> None: + def setEditorData(self, editor: QWidget, index: Union[QModelIndex, QPersistentModelIndex]) -> None: assert isinstance(editor, QLineEdit) value = index.model().data(index, Qt.ItemDataRole.DisplayRole) editor.setText(str(value)) - def setModelData(self, editor: QWidget, model: QAbstractItemModel, index: QModelIndex | QPersistentModelIndex) -> None: + def setModelData(self, editor: QWidget, model: QAbstractItemModel, index: Union[QModelIndex, QPersistentModelIndex]) -> None: step_view = self.parent() assert isinstance(step_view, ProofStepView) assert isinstance(editor, QLineEdit) From ff0467b918f77d0224fbfc28112ec80069f9b583 Mon Sep 17 00:00:00 2001 From: axif Date: Mon, 2 Mar 2026 03:22:25 +0600 Subject: [PATCH 16/19] exact match with previous commit. --- zxlive/commands.py | 26 +++++++++++++------------- zxlive/proof.py | 22 +++++++++++----------- 2 files changed, 24 insertions(+), 24 deletions(-) diff --git a/zxlive/commands.py b/zxlive/commands.py index 68098fef..985d7c15 100644 --- a/zxlive/commands.py +++ b/zxlive/commands.py @@ -4,7 +4,7 @@ from collections import namedtuple from dataclasses import dataclass, field from fractions import Fraction -from typing import Callable, Iterable, Optional, Set, Union, List, Dict, Tuple +from typing import Callable, Iterable, Optional, Set, Union from PySide6.QtCore import QModelIndex from PySide6.QtGui import QUndoCommand @@ -140,14 +140,14 @@ def redo(self) -> None: @dataclass class ChangeNodeType(BaseCommand): """Changes the color of a set of spiders.""" - vs: Union[List[VT], Set[VT]] + vs: list[VT] | set[VT] vty: VertexType WInfo = namedtuple('WInfo', ['partner', 'partner_type', 'partner_pos', 'neighbors']) - _old_vtys: Optional[List[VertexType]] = field(default=None, init=False) - _old_w_info: Optional[Dict[VT, WInfo]] = field(default=None, init=False) - _new_w_inputs: Optional[List[VT]] = field(default=None, init=False) + _old_vtys: Optional[list[VertexType]] = field(default=None, init=False) + _old_w_info: Optional[dict[VT, WInfo]] = field(default=None, init=False) + _new_w_inputs: Optional[list[VT]] = field(default=None, init=False) def undo(self) -> None: assert self._old_vtys is not None @@ -212,7 +212,7 @@ class ChangeEdgeColor(BaseCommand): es: Iterable[ET] ety: EdgeType - _old_etys: Optional[List[EdgeType]] = field(default=None, init=False) + _old_etys: Optional[list[EdgeType]] = field(default=None, init=False) def undo(self) -> None: assert self._old_etys is not None @@ -335,7 +335,7 @@ def redo(self) -> None: @dataclass class AddEdges(BaseCommand): """Adds multiple edges of the same type to a graph.""" - pairs: List[Tuple[VT, VT]] + pairs: list[tuple[VT, VT]] ety: EdgeType def undo(self) -> None: @@ -352,9 +352,9 @@ def redo(self) -> None: @dataclass class MoveNode(BaseCommand): """Updates the location of a collection of nodes.""" - vs: List[Tuple[VT, float, float]] + vs: list[tuple[VT, float, float]] - _old_positions: Optional[List[Tuple[float, float]]] = field(default=None, init=False) + _old_positions: Optional[list[tuple[float, float]]] = field(default=None, init=False) def undo(self) -> None: assert self._old_positions is not None @@ -395,7 +395,7 @@ def redo(self) -> None: @dataclass class MergeNodes(BaseCommand): """Merges groups of vertices that are at the same position.""" - vertices_to_merge: List[VT] + vertices_to_merge: list[VT] _old_g: Optional[GraphT] = field(default=None, init=False) @@ -465,10 +465,10 @@ class AddRewriteStep(UpdateGraph): diff: Optional[GraphDiff] = None _old_selected: Optional[int] = field(default=None, init=False) - _old_steps: List[Tuple[Rewrite, GraphT]] = field(default_factory=list, init=False) + _old_steps: list[tuple[Rewrite, GraphT]] = field(default_factory=list, init=False) # 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: Optional[List[Rewrite]] = field(default=None, init=False) + _old_group_tail: Optional[list[Rewrite]] = field(default=None, init=False) # The original Rewrite object for the group step (before truncation). _old_group_rewrite: Optional[Rewrite] = field(default=None, init=False) @@ -486,7 +486,7 @@ def redo(self) -> None: # Check whether the user is rewriting from inside a grouped sub-step. step_view = self.step_view - sub_step: Optional[Tuple[int, int]] = ( + sub_step: Optional[tuple[int, int]] = ( step_view.selected_sub_step # type: ignore[union-attr] if isinstance(step_view, ProofStepView) else None ) diff --git a/zxlive/proof.py b/zxlive/proof.py index 48c23b2c..cc08f0d9 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -1,7 +1,7 @@ from __future__ import annotations import json -from typing import TYPE_CHECKING, Any, NamedTuple, Optional, Union, Dict, List, Tuple, Set +from typing import TYPE_CHECKING, Any, NamedTuple, Optional, Union, Dict if TYPE_CHECKING: from .proof_panel import ProofPanel @@ -24,7 +24,7 @@ class Rewrite(NamedTuple): display_name: str # Name of proof displayed to user rule: str # Name of the rule that was applied to get to this step graph: GraphT # New graph after applying the rewrite - grouped_rewrites: Optional[List['Rewrite']] = None # Optional field to store the grouped rewrites + grouped_rewrites: Optional[list['Rewrite']] = None # Optional field to store the grouped rewrites def to_dict(self) -> Dict[str, Any]: """Serializes the rewrite to Python dictionary.""" @@ -67,7 +67,7 @@ class ProofModel(QAbstractListModel): """ initial_graph: GraphT - steps: List['Rewrite'] + steps: list['Rewrite'] def __init__(self, start_graph: GraphT): super().__init__() @@ -104,7 +104,7 @@ def set_sub_graph(self, step_idx: int, sub_idx: int, graph: GraphT) -> None: modelIndex = self.createIndex(step_idx + 1, 0) self.dataChanged.emit(modelIndex, modelIndex, []) - def graphs(self) -> List[GraphT]: + def graphs(self) -> list[GraphT]: return [self.initial_graph] + [step.graph for step in self.steps] def data(self, index: Union[QModelIndex, QPersistentModelIndex], role: int = Qt.ItemDataRole.DisplayRole) -> Any: @@ -156,7 +156,7 @@ def add_rewrite(self, rewrite: Rewrite, position: Optional[int] = None) -> None: self.steps.insert(position, rewrite) self.endInsertRows() - def pop_rewrite(self, position: Optional[int] = None) -> Tuple[Rewrite, GraphT]: + def pop_rewrite(self, position: Optional[int] = None) -> tuple[Rewrite, GraphT]: """Removes the latest rewrite from the model. Returns the rewrite and the graph that previously resulted from this rewrite. @@ -292,9 +292,9 @@ def __init__(self, parent: 'ProofPanel'): super().__init__(parent) self.graph_view = parent.graph_view self.undo_stack = parent.undo_stack - self.expanded_groups: Set[int] = set() + self.expanded_groups: set[int] = set() # Track currently selected sub-step: (step_index, sub_step_index) or None - self.selected_sub_step: Optional[Tuple[int, int]] = None + self.selected_sub_step: Optional[tuple[int, int]] = None self._active_sub_editor: Optional[QLineEdit] = None self.setModel(ProofModel(self.graph_view.graph_scene.g)) self.setCurrentIndex(self.model().index(0, 0)) @@ -406,7 +406,7 @@ def _navigate_to_sub_step(self, step_idx: int, sub_idx: int) -> None: model_index = self.model().index(step_idx + 1, 0) self.model().dataChanged.emit(model_index, model_index, []) - def _click_target_for_pos(self, event: QMouseEvent) -> Tuple[int, bool, int]: + def _click_target_for_pos(self, event: QMouseEvent) -> tuple[int, bool, int]: """Classify a mouse-press into (toggle_idx, sub_step_clicked, step_idx). toggle_idx – step index whose triangle was clicked, or -1 @@ -480,7 +480,7 @@ def _repaint_step(self, step_idx: int) -> None: """Trigger repaint for a step row by its 0-based step index.""" self.update(self.model().index(step_idx + 1, 0)) - def _hover_target_for_pos(self, pos: Any) -> Tuple[int, int, int]: + def _hover_target_for_pos(self, pos: Any) -> tuple[int, int, int]: """Return (new_step, new_sub, new_header) for the given mouse position. Each value is -1 when not applicable. @@ -754,7 +754,7 @@ class ProofStepItemDelegate(QStyledItemDelegate): # Track hover over group header hover_header_step_idx: int = -1 - def _step_info(self, index: Union[QModelIndex, QPersistentModelIndex]) -> Tuple[bool, bool, Optional[List['Rewrite']]]: + def _step_info(self, index: Union[QModelIndex, QPersistentModelIndex]) -> tuple[bool, bool, Optional[list['Rewrite']]]: """Return (is_grouped, is_expanded, grouped_rewrites) for a given row.""" if index.row() == 0: return False, False, None @@ -939,7 +939,7 @@ def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QM def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, step_idx: int, - grouped_rewrites: List['Rewrite'], row_height: int, + grouped_rewrites: list['Rewrite'], row_height: int, text_height: int, font: QFont, fg: QColor, line_clr: QColor) -> None: main_cx = self.line_padding + self.line_width / 2 From e438f4ae0c3d660c77c72c42987ceb4515dccedb Mon Sep 17 00:00:00 2001 From: axif Date: Thu, 5 Mar 2026 19:29:19 +0600 Subject: [PATCH 17/19] refactor code implementation ffor proofModel --- zxlive/commands.py | 128 ++---- zxlive/proof.py | 1075 ++++++++++++++------------------------------ 2 files changed, 389 insertions(+), 814 deletions(-) diff --git a/zxlive/commands.py b/zxlive/commands.py index 1577011d..5b983efd 100644 --- a/zxlive/commands.py +++ b/zxlive/commands.py @@ -69,35 +69,16 @@ def __init__(self, command: BaseCommand, step_view: ProofStepView): self.command = command self.step_view = step_view self.proof_step_index = int(step_view.currentIndex().row()) - self.sub_step = step_view.selected_sub_step 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.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) + 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: - self.step_view.move_to_step(self.proof_step_index) + self.step_view.move_to_step(self.proof_step_index) self.command.redo() - 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) + self.step_view.model().set_graph(self.proof_step_index, self.command.g) @dataclass @@ -470,11 +451,8 @@ class AddRewriteStep(UpdateGraph): _old_selected: Optional[int] = field(default=None, init=False) _old_steps: list[tuple[Rewrite, GraphT]] = field(default_factory=list, init=False) - # 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: Optional[list[Rewrite]] = field(default=None, init=False) - # The original Rewrite object for the group step (before truncation). _old_group_rewrite: Optional[Rewrite] = field(default=None, init=False) + _old_sub_idx: int = field(default=-1, init=False) @property def proof_model(self) -> ProofModel: @@ -483,62 +461,36 @@ def proof_model(self) -> ProofModel: return model def redo(self) -> None: - self._old_selected = int(self.step_view.currentIndex().row()) self._old_steps = [] - self._old_group_tail = None self._old_group_rewrite = None + self._old_sub_idx = -1 - # Check whether the user is rewriting from inside a grouped sub-step. - step_view = self.step_view - sub_step: Optional[tuple[int, int]] = ( - step_view.selected_sub_step # type: ignore[union-attr] - if isinstance(step_view, ProofStepView) else None - ) + current = self.step_view.currentIndex() - if sub_step is not None: - group_step_idx, sub_idx = sub_step # 0-based indices into proof_model.steps + # Check if the user is rewriting from inside a grouped sub-step. + if current.parent().isValid() and isinstance(self.step_view, ProofStepView): + parent_row = current.parent().row() + group_step_idx = parent_row - 1 + sub_idx = current.row() + self._old_selected = parent_row + self._old_sub_idx = sub_idx - # 1. Pop all main steps that come AFTER the grouped step (rightmost first). - steps_after_group = self.proof_model.rowCount() - 1 - (group_step_idx + 1) + # 1. Pop all main steps that come AFTER the grouped step. + steps_after_group = self.proof_model.rowCount() - 1 - parent_row for _ in range(steps_after_group): self._old_steps.append(self.proof_model.pop_rewrite()) - # 2. Truncate the grouped step: keep only sub-steps 0..sub_idx (inclusive). - old_group = self.proof_model.steps[group_step_idx] - assert old_group.grouped_rewrites is not None - self._old_group_rewrite = old_group - - kept = old_group.grouped_rewrites[:sub_idx + 1] - self._old_group_tail = old_group.grouped_rewrites[sub_idx + 1:] - - if len(kept) == 1: - # Ungroup: replace the grouped step with the single sub-step. - self.proof_model.pop_rewrite(group_step_idx) - self.proof_model.add_rewrite(kept[0], group_step_idx) - else: - # Update the group in-place with the truncated sub-steps. - new_group = Rewrite( - old_group.display_name, - old_group.rule, - kept[-1].graph, - kept, - ) - self.proof_model.steps[group_step_idx] = new_group - model_index = self.proof_model.createIndex(group_step_idx + 1, 0) - self.proof_model.dataChanged.emit(model_index, model_index, []) - - # Clear the sub-step selection since we are moving outside the group. - if isinstance(step_view, ProofStepView): - step_view.selected_sub_step = None - + # 2. Truncate the grouped step: keep only sub-steps 0..sub_idx. + self._old_group_rewrite = self.proof_model.truncate_group(group_step_idx, sub_idx + 1) else: # Normal case: remove all steps after the currently selected step. + self._old_selected = int(current.row()) for _ in range(self.proof_model.rowCount() - self._old_selected - 1): self._old_steps.append(self.proof_model.pop_rewrite()) self.proof_model.add_rewrite(Rewrite(self.name, self.name, self.new_g)) - # Select the added step. + # Select the added step idx = self.step_view.model().index(self.proof_model.rowCount() - 1, 0, QModelIndex()) self.step_view.selectionModel().blockSignals(True) self.step_view.setCurrentIndex(idx) @@ -546,33 +498,38 @@ def redo(self) -> None: super().redo() def undo(self) -> None: - # Remove the newly added rewrite. + # Undo the rewrite self.step_view.selectionModel().blockSignals(True) self.proof_model.pop_rewrite() self.step_view.selectionModel().blockSignals(False) if self._old_group_rewrite is not None: - # We had truncated (and possibly ungrouped) a group step. - # The group is at group_step_idx == _old_selected - 1. + # Restore the original grouped step (undo truncation/ungrouping). assert self._old_selected is not None group_step_idx = self._old_selected - 1 + self.proof_model.restore_group(group_step_idx, self._old_group_rewrite) - # Remove the current (truncated/ungrouped) step at that position. - self.proof_model.pop_rewrite(group_step_idx) - - # Restore the original grouped step. - self.proof_model.add_rewrite(self._old_group_rewrite, group_step_idx) - - # Restore main steps after the group (they were popped LIFO, restore in reverse). + # Restore main steps that were popped (LIFO order, restore in reverse). for rewrite, graph in reversed(self._old_steps): self.proof_model.add_rewrite(rewrite) - # Restore the previously selected step. + # Select the previously selected step assert self._old_selected is not None - idx = self.step_view.model().index(self._old_selected, 0, QModelIndex()) - self.step_view.selectionModel().blockSignals(True) - self.step_view.setCurrentIndex(idx) - self.step_view.selectionModel().blockSignals(False) + if (self._old_group_rewrite is not None + and self._old_sub_idx >= 0 + and isinstance(self.step_view, ProofStepView)): + # Navigate back into the restored group's sub-step. + parent_idx = self.step_view.model().index(self._old_selected, 0) + self.step_view.expand(parent_idx) + child_idx = self.step_view.model().index(self._old_sub_idx, 0, parent_idx) + self.step_view.selectionModel().blockSignals(True) + self.step_view.setCurrentIndex(child_idx) + self.step_view.selectionModel().blockSignals(False) + else: + idx = self.step_view.model().index(self._old_selected, 0, QModelIndex()) + self.step_view.selectionModel().blockSignals(True) + self.step_view.setCurrentIndex(idx) + self.step_view.selectionModel().blockSignals(False) super().undo() @@ -596,10 +553,13 @@ class UngroupRewriteSteps(BaseCommand): step_view: ProofStepView group_index: int + _group_size: int = field(default=0, init=False) + def redo(self) -> None: + self._group_size = len(self.step_view.model().steps[self.group_index].grouped_rewrites) self.step_view.model().ungroup_steps(self.group_index) self.step_view.move_to_step(self.group_index + 1) def undo(self) -> None: - self.step_view.model().group_steps(self.group_index, self.group_index + 1) + self.step_view.model().group_steps(self.group_index, self.group_index + self._group_size - 1) self.step_view.move_to_step(self.group_index + 1) diff --git a/zxlive/proof.py b/zxlive/proof.py index c00cfbca..74057a9f 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -1,18 +1,17 @@ -from __future__ import annotations - import json from typing import TYPE_CHECKING, Any, NamedTuple, Optional, Union, Dict if TYPE_CHECKING: from .proof_panel import ProofPanel -from PySide6.QtCore import (QAbstractItemModel, QAbstractListModel, +from PySide6.QtCore import (QAbstractItemModel, QEvent, QItemSelection, QModelIndex, QPersistentModelIndex, QPoint, QPointF, QRect, QSize, Qt) -from PySide6.QtGui import QColor, QFont, QFontMetrics, QMouseEvent, QPainter, QPainterPath, QPen, QPolygonF -from PySide6.QtWidgets import (QAbstractItemView, QLineEdit, QListView, QMenu, +from PySide6.QtGui import (QColor, QFont, QFontMetrics, QMouseEvent, QPainter, + QPen, QPolygonF) +from PySide6.QtWidgets import (QAbstractItemView, QLineEdit, QMenu, QStyle, QStyledItemDelegate, - QStyleOptionViewItem, QWidget) + QStyleOptionViewItem, QTreeView, QWidget) from .common import GraphT from .settings import display_setting @@ -59,94 +58,98 @@ def from_json(json_str: Union[str, Dict[str, Any]]) -> "Rewrite": ) -class ProofModel(QAbstractListModel): - """List model capturing the individual steps in a proof. +class ProofModel(QAbstractItemModel): + """Tree model capturing the individual steps in a proof. - There is a row for each graph in the proof sequence. Furthermore, we store the - rewrite that was used to go from one graph to next. + There is a top-level row for each graph sequence. + Grouped rewrites have child rows representing their individual sub-steps. """ initial_graph: GraphT - steps: list['Rewrite'] + steps: list[Rewrite] def __init__(self, start_graph: GraphT): super().__init__() self.initial_graph = start_graph self.steps = [] - def set_graph(self, index: int, graph: GraphT) -> None: - if index == 0: - self.initial_graph = graph - else: - old_step = self.steps[index - 1] - new_step = Rewrite(old_step.display_name, old_step.rule, graph, old_step.grouped_rewrites) - self.steps[index - 1] = new_step - - # Rerender to ensure the model reflects the change immediately - modelIndex = self.createIndex(index, 0) - self.dataChanged.emit(modelIndex, modelIndex, []) - - def set_sub_graph(self, step_idx: int, sub_idx: int, graph: GraphT) -> None: - old_step = self.steps[step_idx] - grouped = old_step.grouped_rewrites - if grouped is None or sub_idx >= len(grouped): - return - - old_sub_step = grouped[sub_idx] - new_sub_step = Rewrite(old_sub_step.display_name, old_sub_step.rule, graph, old_sub_step.grouped_rewrites) - - new_grouped = list(grouped) - new_grouped[sub_idx] = new_sub_step - - self.steps[step_idx] = Rewrite(old_step.display_name, old_step.rule, old_step.graph, new_grouped) + def index(self, row: int, column: int, + parent: Union[QModelIndex, QPersistentModelIndex] = QModelIndex()) -> QModelIndex: + if not self.hasIndex(row, column, parent): + return QModelIndex() + if not parent.isValid(): + return self.createIndex(row, column, 0) + return self.createIndex(row, column, parent.row() + 1) + + def parent(self, child: Union[QModelIndex, QPersistentModelIndex]) -> QModelIndex: + if not child.isValid() or child.internalId() == 0: + return QModelIndex() + return self.createIndex(child.internalId() - 1, 0, 0) + + def rowCount(self, parent: Union[QModelIndex, QPersistentModelIndex] = QModelIndex()) -> int: + if not parent.isValid(): + return len(self.steps) + 1 + if parent.internalId() != 0: + return 0 # No grandchildren + step_idx = parent.row() - 1 + if step_idx < 0 or step_idx >= len(self.steps): + return 0 + grouped = self.steps[step_idx].grouped_rewrites + return len(grouped) if grouped else 0 - # Rerender - modelIndex = self.createIndex(step_idx + 1, 0) - self.dataChanged.emit(modelIndex, modelIndex, []) + def columnCount(self, parent: Union[QModelIndex, QPersistentModelIndex] = QModelIndex()) -> int: + return 1 - def graphs(self) -> list[GraphT]: - return [self.initial_graph] + [step.graph for step in self.steps] + def hasChildren(self, parent: Union[QModelIndex, QPersistentModelIndex] = QModelIndex()) -> bool: + return self.rowCount(parent) > 0 - def data(self, index: Union[QModelIndex, QPersistentModelIndex], role: int = Qt.ItemDataRole.DisplayRole) -> Any: - """Overrides `QAbstractItemModel.data` to populate a view with rewrite steps""" + def _display_name(self, index: Union[QModelIndex, QPersistentModelIndex]) -> Any: + """Return the display name for a model index.""" + if index.internalId() == 0: + if index.row() == 0: + return "START" + step_idx = index.row() - 1 + return self.steps[step_idx].display_name if step_idx < len(self.steps) else None + parent_step_idx = index.internalId() - 2 # internalId = parent_row + 1, step_idx = parent_row - 1 + if 0 <= parent_step_idx < len(self.steps): + grouped = self.steps[parent_step_idx].grouped_rewrites + if grouped and index.row() < len(grouped): + return grouped[index.row()].display_name + return None - if index.row() >= len(self.steps) + 1 or index.column() >= 1: + def data(self, index: Union[QModelIndex, QPersistentModelIndex], + role: int = Qt.ItemDataRole.DisplayRole) -> Any: + if not index.isValid(): return None - if role == Qt.ItemDataRole.DisplayRole: - if index.row() == 0: - return "START" - else: - return self.steps[index.row() - 1].display_name - elif role == Qt.ItemDataRole.FontRole: + return self._display_name(index) + if role == Qt.ItemDataRole.FontRole: return QFont("monospace", 12) + return None def flags(self, index: Union[QModelIndex, QPersistentModelIndex]) -> Qt.ItemFlag: - if index.row() == 0: - return super().flags(index) - return super().flags(index) | Qt.ItemFlag.ItemIsEditable + if not index.isValid(): + return Qt.ItemFlag.NoItemFlags # type: ignore[return-value] + base = Qt.ItemFlag.ItemIsEnabled | Qt.ItemFlag.ItemIsSelectable + if index.internalId() == 0 and index.row() == 0: + return base # type: ignore[return-value] # START not editable + return base | Qt.ItemFlag.ItemIsEditable # type: ignore[return-value] def headerData(self, section: int, orientation: Qt.Orientation, role: int = Qt.ItemDataRole.DisplayRole) -> Any: - """Overrides `QAbstractItemModel.headerData`. - - Indicates that this model doesn't have a header. - """ return None - def columnCount(self, index: Union[QModelIndex, QPersistentModelIndex] = QModelIndex()) -> int: - """The number of columns""" - return 1 - - def rowCount(self, index: 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(): - return len(self.steps) + 1 + def set_graph(self, index: int, graph: GraphT) -> None: + if index == 0: + self.initial_graph = graph else: - return 0 + old = self.steps[index - 1] + self.steps[index - 1] = Rewrite(old.display_name, old.rule, graph, old.grouped_rewrites) + mi = self.createIndex(index, 0, 0) + self.dataChanged.emit(mi, mi, []) + + def graphs(self) -> list[GraphT]: + return [self.initial_graph] + [step.graph for step in self.steps] def add_rewrite(self, rewrite: Rewrite, position: Optional[int] = None) -> None: """Adds a rewrite step to the model.""" @@ -178,16 +181,10 @@ def get_graph(self, index: int) -> GraphT: return copy def rename_step(self, index: int, name: str) -> None: - """Change the display name""" - old_step = self.steps[index] - - # If this is a grouped step whose header contains "→", try to update - # the sub-step display names to stay in sync with the header text. - grouped = old_step.grouped_rewrites + """Change the display name of a step (and sync sub-step names if applicable).""" + old = self.steps[index] + grouped = old.grouped_rewrites if grouped and "\u2192" in name: - # Strip any prefix before the first sub-step name. - # The auto-generated format is "Prefix: sub1 → sub2 → ...", - # so we split on ": " once to separate the prefix. body = name.split(": ", 1)[-1] if ": " in name else name sub_names = [s.strip() for s in body.split("\u2192")] if len(sub_names) == len(grouped): @@ -196,35 +193,23 @@ def rename_step(self, index: int, name: str) -> None: if sub_names[i] != rw.display_name else rw for i, rw in enumerate(grouped) ] - - # Must create a new Rewrite object instead of modifying current object - # since Rewrite inherits NamedTuple and is hence immutable - self.steps[index] = Rewrite(name, old_step.rule, old_step.graph, grouped) - - # Rerender the proof step otherwise it will display the old name until - # the cursor moves - modelIndex = self.createIndex(index + 1, 0) - self.dataChanged.emit(modelIndex, modelIndex, []) + self.steps[index] = Rewrite(name, old.rule, old.graph, grouped) + mi = self.createIndex(index + 1, 0, 0) + self.dataChanged.emit(mi, mi, []) def rename_sub_step(self, step_index: int, sub_index: int, name: str) -> None: - """Change the display name of a sub-step""" - old_step = self.steps[step_index] - grouped = old_step.grouped_rewrites + """Change the display name of a sub-step.""" + old = self.steps[step_index] + grouped = old.grouped_rewrites if grouped is None or sub_index >= len(grouped): return - - old_sub_step = grouped[sub_index] - new_sub_step = Rewrite(name, old_sub_step.rule, old_sub_step.graph, old_sub_step.grouped_rewrites) - + old_sub = grouped[sub_index] new_grouped = list(grouped) - new_grouped[sub_index] = new_sub_step - - # Update the main step's grouped rewrites - self.steps[step_index] = Rewrite(old_step.display_name, old_step.rule, old_step.graph, new_grouped) - - # Rerender - modelIndex = self.createIndex(step_index + 1, 0) - self.dataChanged.emit(modelIndex, modelIndex, []) + new_grouped[sub_index] = Rewrite(name, old_sub.rule, old_sub.graph, old_sub.grouped_rewrites) + self.steps[step_index] = Rewrite(old.display_name, old.rule, old.graph, new_grouped) + parent_mi = self.index(step_index + 1, 0) + child_mi = self.index(sub_index, 0, parent_mi) + self.dataChanged.emit(child_mi, child_mi, []) def group_steps(self, start_index: int, end_index: int) -> None: """Replace the individual steps from `start_index` to `end_index` with a new grouped step""" @@ -235,10 +220,8 @@ def group_steps(self, start_index: int, end_index: int) -> None: self.steps[start_index:end_index + 1] ) for _ in range(end_index - start_index + 1): - self.pop_rewrite(start_index)[0] + self.pop_rewrite(start_index) self.add_rewrite(new_rewrite, start_index) - modelIndex = self.createIndex(start_index + 1, 0) - self.dataChanged.emit(modelIndex, modelIndex, []) def ungroup_steps(self, index: int) -> None: """Replace the grouped step at `index` with the individual_steps""" @@ -248,18 +231,49 @@ def ungroup_steps(self, index: int) -> None: self.pop_rewrite(index) for i, step in enumerate(individual_steps): self.add_rewrite(step, index + i) - self.dataChanged.emit(self.createIndex(index + 1, 0), - self.createIndex(index + len(individual_steps), 0), - []) + def truncate_group(self, step_index: int, keep_count: int) -> 'Rewrite': + """Truncate a grouped step, keeping only the first `keep_count` sub-steps. + + If keep_count == 1 the group is replaced by the single remaining sub-step + (i.e. the group is "ungrouped"). Returns the *original* Rewrite so that + the caller can restore it later via `restore_group`. + """ + old = self.steps[step_index] + assert old.grouped_rewrites is not None + assert 0 < keep_count <= len(old.grouped_rewrites) + + kept = old.grouped_rewrites[:keep_count] + + if keep_count == 1: + # Ungroup: replace the grouped step with the single sub-step. + self.pop_rewrite(step_index) + self.add_rewrite(kept[0], step_index) + else: + # Shrink in-place, notifying the tree view about removed children. + parent_idx = self.index(step_index + 1, 0) + n_old = len(old.grouped_rewrites) + if keep_count < n_old: + self.beginRemoveRows(parent_idx, keep_count, n_old - 1) + self.steps[step_index] = Rewrite( + old.display_name, old.rule, kept[-1].graph, kept, + ) + if keep_count < n_old: + self.endRemoveRows() + mi = self.createIndex(step_index + 1, 0, 0) + self.dataChanged.emit(mi, mi, []) + + return old + + def restore_group(self, step_index: int, original: 'Rewrite') -> None: + """Restore a previously truncated / ungrouped step to its original group.""" + self.pop_rewrite(step_index) + self.add_rewrite(original, step_index) def to_dict(self) -> Dict[str, Any]: """Serializes the model to Python dict.""" - initial_graph = self.initial_graph.to_dict() - proof_steps = [step.to_dict() for step in self.steps] - return { - "initial_graph": initial_graph, - "proof_steps": proof_steps + "initial_graph": self.initial_graph.to_dict(), + "proof_steps": [step.to_dict() for step in self.steps] } def to_json(self) -> str: @@ -280,45 +294,44 @@ def from_json(json_str: Union[str, Dict[str, Any]]) -> "ProofModel": initial_graph.set_auto_simplify(False) model = ProofModel(initial_graph) for step in d["proof_steps"]: - rewrite = Rewrite.from_json(step) - model.add_rewrite(rewrite) + model.add_rewrite(Rewrite.from_json(step)) return model -class ProofStepView(QListView): +class ProofStepView(QTreeView): """A view for displaying the steps in a proof.""" def __init__(self, parent: 'ProofPanel'): super().__init__(parent) self.graph_view = parent.graph_view self.undo_stack = parent.undo_stack - self.expanded_groups: set[int] = set() - # Track currently selected sub-step: (step_index, sub_step_index) or None - self.selected_sub_step: Optional[tuple[int, int]] = None - self._active_sub_editor: Optional[QLineEdit] = None self.setModel(ProofModel(self.graph_view.graph_scene.g)) self.setCurrentIndex(self.model().index(0, 0)) + + # Tree config: all visual layout handled by our delegate + self.setIndentation(0) + self.setRootIsDecorated(False) + self.setItemsExpandable(False) + self.setExpandsOnDoubleClick(False) + self.setHeaderHidden(True) 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 + + # Styling pal = self.palette() if display_setting.dark_mode: + self.setStyleSheet("background-color: #23272e;") pal.setColor(self.backgroundRole(), QColor(35, 39, 46)) pal.setColor(self.viewport().backgroundRole(), QColor(35, 39, 46)) else: + self.setStyleSheet("") 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.setUniformRowHeights(True) self.setAlternatingRowColors(True) self.viewport().setAttribute(Qt.WidgetAttribute.WA_Hover) self.setContextMenuPolicy(Qt.ContextMenuPolicy.CustomContextMenu) @@ -334,334 +347,58 @@ def model(self) -> ProofModel: 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() - - 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. + def move_to_step(self, index: int) -> None: + idx = self.model().index(index, 0, QModelIndex()) + self.setCurrentIndex(idx) - 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) - - def _navigate_to_sub_step(self, step_idx: int, sub_idx: int) -> None: - """Display the graph corresponding to a sub-step within a grouped rewrite.""" - step = self.model().steps[step_idx] - if step.grouped_rewrites is None or sub_idx < 0 or sub_idx >= len(step.grouped_rewrites): + def proof_step_selected(self, selected: QItemSelection, deselected: QItemSelection) -> None: + if not selected: return - self.selected_sub_step = (step_idx, sub_idx) - sub_graph = step.grouped_rewrites[sub_idx].graph.copy() - assert isinstance(sub_graph, GraphT) - self.graph_view.set_graph(sub_graph) - # Trigger repaint so the delegate can highlight the selected sub-step - model_index = self.model().index(step_idx + 1, 0) - self.model().dataChanged.emit(model_index, model_index, []) - - def _click_target_for_pos(self, event: QMouseEvent) -> tuple[int, bool, int]: - """Classify a mouse-press into (toggle_idx, sub_step_clicked, step_idx). - - toggle_idx – step index whose triangle was clicked, or -1 - sub_step_clicked – True when a sub-step row was clicked - step_idx – the step row the click landed on (only meaningful - when toggle_idx >= 0 or sub_step_clicked is True) - """ - index = self.indexAt(event.pos()) - if not index.isValid() or index.row() <= 0: - return -1, False, -1 - step_idx = index.row() - 1 - if step_idx >= len(self.model().steps): - return -1, False, -1 - step = self.model().steps[step_idx] - if step.grouped_rewrites is None: - return -1, False, -1 - delegate = self.itemDelegate() - if not isinstance(delegate, ProofStepItemDelegate): - return -1, False, -1 - rect = self.visualRect(index) - if self._triangle_hit_test(step_idx, int(event.pos().x()), int(event.pos().y()), - rect.x(), rect.y()): - return step_idx, False, step_idx # triangle clicked → toggle - if step_idx in self.expanded_groups: - sub_idx = self._sub_step_hit_test(step_idx, int(event.pos().y()), rect.y()) - if sub_idx >= 0: - self._navigate_to_sub_step(step_idx, sub_idx) - return -1, True, step_idx # sub-step clicked - return -1, False, -1 - - def mousePressEvent(self, event: QMouseEvent) -> None: # type: ignore[override] - """Handle mouse clicks on grouped steps to toggle expansion. - - Only clicking on the triangle triggers expand/collapse. - Clicking on a sub-step navigates to that sub-step's graph. - """ - index = self.indexAt(event.pos()) - # Save old sub-step selection; if the user clicks a sub-step in a - # different group we need to repaint the old group's row to clear - # its stale highlight. - old_sub_step = self.selected_sub_step - - toggle_idx, sub_step_clicked, step_idx = self._click_target_for_pos(event) - - # Clear sub-step selection when clicking on a non-sub-step area - if not sub_step_clicked and self.selected_sub_step is not None: - old_step_idx = self.selected_sub_step[0] - self.selected_sub_step = None - old_model_idx = self.model().index(old_step_idx + 1, 0) - self.model().dataChanged.emit(old_model_idx, old_model_idx, []) - - if sub_step_clicked: - # Repaint the old group's row if we switched from a different group, - # so the stale sub-step highlight is cleared. - if old_sub_step is not None and old_sub_step[0] != step_idx: - old_model_idx = self.model().index(old_sub_step[0] + 1, 0) - self.model().dataChanged.emit(old_model_idx, old_model_idx, []) - # Select the parent row in QListView so it appears as the active - # step, but block signals to prevent proof_step_selected from - # overwriting the sub-step graph we just navigated to. - self.selectionModel().blockSignals(True) - self.setCurrentIndex(index) - self.selectionModel().blockSignals(False) - else: - super().mousePressEvent(event) - - if toggle_idx >= 0: - self.toggle_group_expansion(toggle_idx) - - def _repaint_step(self, step_idx: int) -> None: - """Trigger repaint for a step row by its 0-based step index.""" - self.update(self.model().index(step_idx + 1, 0)) - - def _hover_target_for_pos(self, pos: Any) -> tuple[int, int, int]: - """Return (new_step, new_sub, new_header) for the given mouse position. - - Each value is -1 when not applicable. - """ - index = self.indexAt(pos) - if not index.isValid() or index.row() <= 0: - return -1, -1, -1 - step_idx = index.row() - 1 - if step_idx >= len(self.model().steps): - return -1, -1, -1 - step = self.model().steps[step_idx] - if step.grouped_rewrites is None: - return -1, -1, -1 - if step_idx not in self.expanded_groups: - return -1, -1, step_idx - rect = self.visualRect(index) - sub_idx = self._sub_step_hit_test(step_idx, int(pos.y()), rect.y()) - if sub_idx >= 0: - return step_idx, sub_idx, -1 - return -1, -1, step_idx - - def mouseMoveEvent(self, event: QMouseEvent) -> None: # type: ignore[override] - """Track which sub-step the mouse is hovering over and trigger repaint.""" - delegate = self.itemDelegate() - if not isinstance(delegate, ProofStepItemDelegate): - super().mouseMoveEvent(event) + index = selected.first().topLeft() + if not index.isValid(): return - - old_step = delegate.hover_step_idx - old_sub = delegate.hover_sub_idx - old_header = delegate.hover_header_step_idx - new_step, new_sub, new_header = self._hover_target_for_pos(event.pos()) - - if new_step != old_step or new_sub != old_sub: - delegate.hover_step_idx = new_step - delegate.hover_sub_idx = new_sub - if old_step >= 0: - self._repaint_step(old_step) - if new_step >= 0: - self._repaint_step(new_step) - - if new_header != old_header: - delegate.hover_header_step_idx = new_header - if old_header >= 0: - self._repaint_step(old_header) - if new_header >= 0: - self._repaint_step(new_header) - - if new_sub >= 0: - self.setCursor(Qt.CursorShape.PointingHandCursor) + if index.parent().isValid(): + # Sub-step clicked → show sub-step graph natively + step_idx = index.parent().row() - 1 + sub_idx = index.row() + step = self.model().steps[step_idx] + if step.grouped_rewrites and sub_idx < len(step.grouped_rewrites): + self.graph_view.set_graph(step.grouped_rewrites[sub_idx].graph.copy()) else: - self.unsetCursor() - - super().mouseMoveEvent(event) - - def leaveEvent(self, event: Any) -> None: - """Clear sub-step hover state when the mouse leaves the widget.""" - delegate = self.itemDelegate() - if isinstance(delegate, ProofStepItemDelegate): - old_step = delegate.hover_step_idx - old_header = delegate.hover_header_step_idx - delegate.hover_step_idx = -1 - delegate.hover_sub_idx = -1 - delegate.hover_header_step_idx = -1 - if old_step >= 0: - self._repaint_step(old_step) - if old_header >= 0: - self._repaint_step(old_header) - self.unsetCursor() - super().leaveEvent(event) + self.graph_view.set_graph(self.model().get_graph(index.row())) - def move_to_step(self, index: int) -> None: - idx = self.model().index(index, 0, QModelIndex()) - self.clearSelection() - self.selectionModel().blockSignals(True) - self.setCurrentIndex(idx) - self.selectionModel().blockSignals(False) - self.update(idx) - g = self.model().get_graph(index) - self.graph_view.set_graph(g) + # Context menu def show_context_menu(self, position: QPoint) -> None: - selected_indexes = self.selectedIndexes() - if not selected_indexes: + index = self.indexAt(position) + if not index.isValid(): return context_menu = QMenu(self) - action_function_map = {} - - index = selected_indexes[0].row() - if len(selected_indexes) > 1: - group_action = context_menu.addAction("Group Steps") - action_function_map[group_action] = self.group_selected_steps - elif index != 0: - rename_action = context_menu.addAction("Rename Step") - action_function_map[rename_action] = lambda: self.edit(selected_indexes[0]) - if self.model().steps[index - 1].grouped_rewrites is not None: - ungroup_action = context_menu.addAction("Ungroup Steps") - action_function_map[ungroup_action] = self.ungroup_selected_step - - # Check if we clicked on a sub-step - step_idx = index - 1 - if step_idx in self.expanded_groups: - rect = self.visualRect(selected_indexes[0]) - # We need the relative position within the item rect - # mapToGlobal(position) is global, position is local to widget - # position is passed from customContextMenuRequested, which is in widget coords - sub_idx = self._sub_step_hit_test( - step_idx, int(position.y()), rect.y() - ) - if sub_idx >= 0: - # If a sub-step is clicked, we probably want to rename the sub-step, - # not the parent group step. - context_menu.removeAction(rename_action) - rename_sub_action = context_menu.addAction("Rename Sub-step") - action_function_map[rename_sub_action] = lambda: self._open_sub_step_editor(step_idx, sub_idx) - - action = context_menu.exec_(self.mapToGlobal(position)) - if action in action_function_map: - action_function_map[action]() - - def _open_sub_step_editor(self, step_idx: int, sub_idx: int) -> None: - """Opens an inline editor for renaming a sub-step.""" - delegate = self.itemDelegate() - if not isinstance(delegate, ProofStepItemDelegate): - return + action_map: dict[Any, Any] = {} - # 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; }") + if index.parent().isValid(): + # Right-clicked on a sub-step + rename_action = context_menu.addAction("Rename Sub-step") + action_map[rename_action] = lambda: self.edit(index) else: - editor.setStyleSheet("QLineEdit { background-color: white; color: black; border: 1px solid #ccc; }") + top_level = [i for i in self.selectedIndexes() if not i.parent().isValid()] + if len(top_level) > 1: + action_map[context_menu.addAction("Group Steps")] = self.group_selected_steps + elif index.row() != 0: + action_map[context_menu.addAction("Rename Step")] = lambda: self.edit(index) + step_idx = index.row() - 1 + if step_idx < len(self.model().steps) and self.model().steps[step_idx].grouped_rewrites is not None: + action_map[context_menu.addAction("Ungroup Steps")] = self.ungroup_selected_step - # 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 + action = context_menu.exec_(self.mapToGlobal(position)) + if action in action_map: + action_map[action]() - def _finish_sub_step_edit(self, step_idx: int, sub_idx: int, editor: QLineEdit) -> None: - if not editor.isVisible(): - # Already finished/deleted - return - new_name = editor.text() - self.rename_proof_sub_step(new_name, step_idx, sub_idx) - editor.deleteLater() - self._active_sub_editor = None + # Rename def rename_proof_sub_step(self, new_name: str, step_index: int, sub_index: int) -> None: from .commands import UndoableChange @@ -682,57 +419,39 @@ def rename_proof_step(self, new_name: str, index: int) -> None: lambda: self.model().rename_step(index, new_name)) self.undo_stack.push(cmd) - def proof_step_selected(self, selected: QItemSelection, deselected: QItemSelection) -> None: - if not selected or not deselected: - return - # Clear sub-step selection when a different main step is selected - if self.selected_sub_step is not None: - old_step_idx = self.selected_sub_step[0] - self.selected_sub_step = None - old_model_idx = self.model().index(old_step_idx + 1, 0) - self.model().dataChanged.emit(old_model_idx, old_model_idx, []) - step_index = selected.first().topLeft().row() - self.move_to_step(step_index) + # Group / Ungroup def group_selected_steps(self) -> None: from .commands import GroupRewriteSteps from .dialogs import show_error_msg - selected_indexes = self.selectedIndexes() - if not selected_indexes or len(selected_indexes) < 2: + selected = sorted(i.row() for i in self.selectedIndexes() if not i.parent().isValid()) + if len(selected) < 2: raise ValueError("Can only group two or more steps") - - indices = sorted(index.row() for index in selected_indexes) - if indices[-1] - indices[0] != len(indices) - 1: + if selected[-1] - selected[0] != len(selected) - 1: show_error_msg("Can only group contiguous steps") raise ValueError("Can only group contiguous steps") - if indices[0] == 0: + if selected[0] == 0: show_error_msg("Cannot group the first step") raise ValueError("Cannot group the first step") - - self.move_to_step(indices[-1] - 1) - cmd = GroupRewriteSteps(self.graph_view, self, indices[0] - 1, indices[-1] - 1) - self.undo_stack.push(cmd) + self.move_to_step(selected[-1] - 1) + self.undo_stack.push(GroupRewriteSteps(self.graph_view, self, selected[0] - 1, selected[-1] - 1)) def ungroup_selected_step(self) -> None: from .commands import UngroupRewriteSteps - selected_indexes = self.selectedIndexes() - if not selected_indexes or len(selected_indexes) != 1: + top_level = [i for i in self.selectedIndexes() if not i.parent().isValid()] + if len(top_level) != 1: raise ValueError("Can only ungroup one step") - - index = selected_indexes[0].row() - if index == 0 or self.model().steps[index - 1].grouped_rewrites is None: + row = top_level[0].row() + if row == 0 or self.model().steps[row - 1].grouped_rewrites is None: raise ValueError("Step is not grouped") - - self.move_to_step(index - 1) - cmd = UngroupRewriteSteps(self.graph_view, self, index - 1) - self.undo_stack.push(cmd) + self.move_to_step(row - 1) + self.undo_stack.push(UngroupRewriteSteps(self.graph_view, self, row - 1)) class ProofStepItemDelegate(QStyledItemDelegate): """This class controls the painting of items in the proof steps list view. We paint a "git-style" line with circles to denote individual steps in a proof. - Grouped steps render as expandable tree nodes with sub-step branches. """ line_width = 3 @@ -743,313 +462,209 @@ class ProofStepItemDelegate(QStyledItemDelegate): circle_radius_selected = 6 circle_outline_width = 3 - # TODO: Fix code complexity - # noqa: complexipy - # Sub-tree layout for expanded groups triangle_size = 5 sub_indent = 20 - sub_branch_len = 15 - - # Track hover position for sub-steps - hover_step_idx: int = -1 - hover_sub_idx: int = -1 - # Track hover over group header - hover_header_step_idx: int = -1 - - def _step_info(self, index: Union[QModelIndex, QPersistentModelIndex]) -> tuple[bool, bool, Optional[list['Rewrite']]]: - """Return (is_grouped, is_expanded, grouped_rewrites) for a given row.""" - if index.row() == 0: - return False, False, None - model = index.model() - if not isinstance(model, ProofModel): - return False, False, None - step_idx = index.row() - 1 - if step_idx >= len(model.steps): - return False, False, None - step = model.steps[step_idx] - if step.grouped_rewrites is None: - return False, False, None - view = self.parent() - is_expanded = isinstance(view, ProofStepView) and step_idx in view.expanded_groups - return True, is_expanded, step.grouped_rewrites + + def editorEvent(self, event: QEvent, model: QAbstractItemModel, + option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> bool: + """Handle triangle clicks natively within the delegate's event flow without view coordinate tracking.""" + if event.type() == QEvent.Type.MouseButtonPress and isinstance(event, QMouseEvent): + step_view = self.parent() + if isinstance(step_view, QTreeView): + rect = option.rect # type: ignore[attr-defined] + text_h = QFontMetrics(option.font).height() # type: ignore[attr-defined] + row_h = text_h + 2 * self.vert_padding + text_x = rect.x() + self.line_width + 2 * self.line_padding + cy = rect.y() + row_h / 2 + s = self.triangle_size + + pos = event.pos() + # Check hit test using native option rect properties + if text_x <= pos.x() <= text_x + s * 2 and cy - s <= pos.y() <= cy + s: + if not index.parent().isValid() and model.hasChildren(index): + step_view.setCurrentIndex(index) + step_view.setExpanded(index, not step_view.isExpanded(index)) + return True + return super().editorEvent(event, model, option, index) @staticmethod - def _bg_color(selected: bool, sub_selected: bool, hovered: bool) -> QColor: - """Return the background color for the given state.""" - if display_setting.dark_mode: - if selected: - return QColor(60, 80, 120) - if sub_selected: - return QColor(45, 50, 60) - if hovered: - return QColor(50, 60, 80) - return QColor(35, 39, 46) + def _bg_color(selected: bool, hovered: bool) -> QColor: + """Return background color for the given state.""" + dark = display_setting.dark_mode if selected: - return QColor(204, 232, 255) - if sub_selected: - return QColor(240, 245, 250) + return QColor(60, 80, 120) if dark else QColor(204, 232, 255) if hovered: - return QColor(229, 243, 255) - return QColor(255, 255, 255) + return QColor(50, 60, 80) if dark else QColor(229, 243, 255) + return QColor(35, 39, 46) if dark else QColor(255, 255, 255) - def paint(self, painter: QPainter, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> None: # noqa: PLR0912 + def paint(self, painter: QPainter, option: QStyleOptionViewItem, + index: Union[QModelIndex, QPersistentModelIndex]) -> None: painter.save() painter.setRenderHint(QPainter.RenderHint.Antialiasing) - is_grouped, is_expanded, grouped_rewrites = self._step_info(index) + is_selected = bool(option.state & QStyle.StateFlag.State_Selected) # type: ignore[attr-defined] + is_hovered = bool(option.state & QStyle.StateFlag.State_MouseOver) # type: ignore[attr-defined] + + # Background + painter.setPen(Qt.GlobalColor.transparent) + painter.setBrush(self._bg_color(is_selected, is_hovered)) + painter.drawRect(option.rect) # type: ignore[attr-defined] font = QFont(option.font) # type: ignore[attr-defined] - text_height = QFontMetrics(font).height() - row_height = text_height + 2 * self.vert_padding + text_h = QFontMetrics(font).height() + row_h = text_h + 2 * self.vert_padding fg = QColor(224, 224, 224) if display_setting.dark_mode else QColor(0, 0, 0) line_clr = QColor(180, 180, 180) if display_setting.dark_mode else QColor(0, 0, 0) - # Check if a sub-step is selected in this grouped rewrite - view = self.parent() - has_selected_sub_step = False - if isinstance(view, ProofStepView) and view.selected_sub_step is not None: - sel_step_idx, _ = view.selected_sub_step - if index.row() - 1 == sel_step_idx: - has_selected_sub_step = True - - # ── Background ────────────────────────────────────────────────── - is_selected = bool(option.state & QStyle.StateFlag.State_Selected) # type: ignore[attr-defined] - is_mouse_over = bool(option.state & QStyle.StateFlag.State_MouseOver) # type: ignore[attr-defined] - is_header_hovered = (is_grouped - and index.row() > 0 - and self.hover_header_step_idx == index.row() - 1) - - bg = self._bg_color(is_selected, has_selected_sub_step, is_mouse_over) - neutral_bg = self._bg_color(False, False, False) - - painter.setPen(Qt.GlobalColor.transparent) - if is_expanded: - # Fill entire area with neutral, then highlight just the header row - painter.setBrush(neutral_bg) - painter.drawRect(option.rect) # type: ignore[attr-defined] - if is_selected or has_selected_sub_step or is_header_hovered: - header_bg = self._bg_color(is_selected, has_selected_sub_step, is_header_hovered) - painter.setBrush(header_bg) - painter.drawRect(QRect( - option.rect.x(), option.rect.y(), # type: ignore[attr-defined] - option.rect.width(), row_height)) # type: ignore[attr-defined] + if index.parent().isValid(): + self._paint_child(painter, option, index, font, text_h, row_h, fg, line_clr) else: - painter.setBrush(bg) - painter.drawRect(option.rect) # type: ignore[attr-defined] + self._paint_toplevel(painter, option, index, font, text_h, row_h, fg, line_clr) - # ── Main timeline line ────────────────────────────────────────── - is_last = index.row() == index.model().rowCount() - 1 + painter.restore() + + def _paint_toplevel(self, painter: QPainter, option: QStyleOptionViewItem, + index: Union[QModelIndex, QPersistentModelIndex], + font: QFont, text_h: int, row_h: int, + fg: QColor, line_clr: QColor) -> None: + """Paint a top-level step on the main timeline.""" + rect = option.rect # type: ignore[attr-defined] + main_cx = self.line_padding + self.line_width / 2 + circle_cy = rect.y() + row_h / 2 - # Use a Pen with RoundCap for lines to allow smooth overlaps with neighbor - # segments and the diverted path. pen = QPen(line_clr, self.line_width) pen.setCapStyle(Qt.PenCapStyle.RoundCap) painter.setPen(pen) painter.setBrush(Qt.GlobalColor.transparent) - circle_cy = option.rect.y() + row_height / 2 # type: ignore[attr-defined] - main_cx = self.line_padding + self.line_width / 2 + # Line: top → circle + painter.drawLine(QPointF(main_cx, rect.y()), QPointF(main_cx, circle_cy)) + + # Check grouped & expanded + is_grouped = False + is_expanded = False + model = index.model() + if isinstance(model, ProofModel) and index.row() > 0: + step_idx = index.row() - 1 + if step_idx < len(model.steps) and model.steps[step_idx].grouped_rewrites: + is_grouped = True + view = self.parent() + is_expanded = isinstance(view, QTreeView) and view.isExpanded(index) + + is_last = index.row() == index.model().rowCount() - 1 - # Draw line from top to center - painter.drawLine(QPointF(main_cx, option.rect.y()), QPointF(main_cx, circle_cy)) # type: ignore[attr-defined] - - # For expanded groups, draw the sub-tree BEFORE the circle so the - # path doesn't draw over the circle. - if is_expanded and grouped_rewrites: - self._paint_sub_tree(painter, option, index.row() - 1, - grouped_rewrites, - row_height, text_height, font, fg, line_clr) - - # Draw bottom half of line (from center of circle to bottom) - # Only if NOT expanded (if expanded, the line diverts to the sub-steps) - if not is_expanded: - bottom_y = option.rect.y() + option.rect.height() # type: ignore[attr-defined] - if not is_last: - painter.setPen(pen) - painter.setBrush(Qt.GlobalColor.transparent) - painter.drawLine(QPointF(main_cx, circle_cy), QPointF(main_cx, bottom_y)) - - # ── Main circle ───────────────────────────────────────────────── - circle_cy = option.rect.y() + row_height / 2 # type: ignore[attr-defined] + # Line: circle → bottom + if is_expanded: + painter.drawLine(QPointF(main_cx, circle_cy), + QPointF(main_cx + self.sub_indent, rect.y() + rect.height())) + elif not is_last: + painter.drawLine(QPointF(main_cx, circle_cy), + QPointF(main_cx, rect.y() + rect.height())) + + # Circle painter.setPen(QPen(line_clr, self.circle_outline_width)) painter.setBrush(display_setting.effective_colors["z_spider"]) cr = self.circle_radius_selected \ if option.state & QStyle.StateFlag.State_Selected else self.circle_radius # type: ignore[attr-defined] - main_cx = self.line_padding + self.line_width / 2 painter.drawEllipse(QPointF(main_cx, circle_cy), cr, cr) - # ── Text / group indicator ────────────────────────────────────── - text_x_base = int(option.rect.x() + self.line_width + 2 * self.line_padding) # type: ignore[attr-defined] - + # Text (with optional triangle for groups) + text_x = int(rect.x() + self.line_width + 2 * self.line_padding) if is_grouped: s = self.triangle_size - tri_cy = int(option.rect.y() + row_height / 2) # type: ignore[attr-defined] + tri_cy = int(rect.y() + row_h / 2) painter.setPen(Qt.GlobalColor.transparent) painter.setBrush(fg) - if is_expanded: - # Down-pointing triangle ▼ - triangle = QPolygonF([ - QPointF(text_x_base, tri_cy - s * 0.5), - QPointF(text_x_base + s * 2, tri_cy - s * 0.5), - QPointF(text_x_base + s, tri_cy + s * 0.5 + 1), - ]) + tri = QPolygonF([QPointF(text_x, tri_cy - s * 0.5), + QPointF(text_x + s * 2, tri_cy - s * 0.5), + QPointF(text_x + s, tri_cy + s * 0.5 + 1)]) else: - # Right-pointing triangle ▶ - triangle = QPolygonF([ - QPointF(text_x_base, tri_cy - s), - QPointF(text_x_base + s, tri_cy), - QPointF(text_x_base, tri_cy + s), - ]) - painter.drawPolygon(triangle) - - tri_offset = s * 2 + 4 - # Always show the actual display name, not hardcoded "Grouped Steps" - header_text = index.data(Qt.ItemDataRole.DisplayRole) - text_rect = QRect( - text_x_base + tri_offset, - int(option.rect.y() + row_height / 2 - text_height / 2), # type: ignore[attr-defined] - int(option.rect.width() - self.line_width - 2 * self.line_padding - tri_offset), # type: ignore[attr-defined] - text_height - ) - # Only make bold if selected, not just because it's grouped - draw_font = QFont(font) - if option.state & QStyle.StateFlag.State_Selected: # type: ignore[attr-defined] - draw_font.setWeight(QFont.Weight.Bold) - painter.setFont(draw_font) - painter.setPen(fg) - painter.drawText(text_rect, Qt.AlignmentFlag.AlignLeft, header_text) - - # Sub-tree was already drawn above (before the circle) for expanded groups - else: - # Regular (non-grouped) step text - text = index.data(Qt.ItemDataRole.DisplayRole) - text_rect = QRect( - text_x_base, - int(option.rect.y() + row_height / 2 - text_height / 2), # type: ignore[attr-defined] - int(option.rect.width() - self.line_width - 2 * self.line_padding), # type: ignore[attr-defined] - text_height - ) - draw_font = QFont(font) - if option.state & QStyle.StateFlag.State_Selected: # type: ignore[attr-defined] - draw_font.setWeight(QFont.Weight.Bold) - painter.setFont(draw_font) - painter.setPen(fg) - painter.drawText(text_rect, Qt.AlignmentFlag.AlignLeft, text) - - painter.restore() - - def _paint_sub_tree(self, painter: QPainter, option: QStyleOptionViewItem, - step_idx: int, - grouped_rewrites: list['Rewrite'], row_height: int, - text_height: int, font: QFont, - fg: QColor, line_clr: QColor) -> None: + tri = QPolygonF([QPointF(text_x, tri_cy - s), + QPointF(text_x + s, tri_cy), + QPointF(text_x, tri_cy + s)]) + painter.drawPolygon(tri) + text_x += s * 2 + 4 + + draw_font = QFont(font) + if option.state & QStyle.StateFlag.State_Selected: # type: ignore[attr-defined] + draw_font.setWeight(QFont.Weight.Bold) + painter.setFont(draw_font) + painter.setPen(fg) + painter.drawText( + QRect(text_x, int(rect.y() + row_h / 2 - text_h / 2), + int(rect.width() - text_x + rect.x()), text_h), + Qt.AlignmentFlag.AlignLeft, + index.data(Qt.ItemDataRole.DisplayRole)) + + def _paint_child(self, painter: QPainter, option: QStyleOptionViewItem, + index: Union[QModelIndex, QPersistentModelIndex], + font: QFont, text_h: int, row_h: int, + fg: QColor, line_clr: QColor) -> None: + """Paint a sub-step on the branch line.""" + rect = option.rect # type: ignore[attr-defined] main_cx = self.line_padding + self.line_width / 2 - sub_tree_x = main_cx + self.sub_indent - n = len(grouped_rewrites) - - header_cy = option.rect.y() + row_height / 2 # type: ignore[attr-defined] - first_sub_cy = option.rect.y() + row_height + row_height / 2 # type: ignore[attr-defined] - last_sub_cy = option.rect.y() + row_height + (n - 1) * row_height + row_height / 2 # type: ignore[attr-defined] - bottom_y = option.rect.y() + option.rect.height() # type: ignore[attr-defined] - - # 1. Draw sub-step highlights first so they sit in the background - for i, sub_step in enumerate(grouped_rewrites): - sub_cy = first_sub_cy + i * row_height - is_sub_selected = False - # Determine which sub-step is selected (if any) - view = self.parent() - if isinstance(view, ProofStepView) and view.selected_sub_step is not None: - sel_step_idx, sel_sub_idx = view.selected_sub_step - if step_idx == sel_step_idx and i == sel_sub_idx: - is_sub_selected = True - - # Check if this sub-step is being hovered (for individual hover effect) - is_sub_hovered = (self.hover_step_idx == step_idx and self.hover_sub_idx == i) - - # Highlight spans the full width of the item, starting from the left edge - if is_sub_selected or is_sub_hovered: - painter.setPen(Qt.GlobalColor.transparent) - painter.setBrush(self._bg_color(is_sub_selected, False, is_sub_hovered)) - painter.drawRect(QRect( - option.rect.x(), int(sub_cy - row_height / 2), # type: ignore[attr-defined] - option.rect.width(), row_height)) # type: ignore[attr-defined] - - # 2. Draw the path connecting header -> sub-steps -> next step + branch_x = main_cx + self.sub_indent + circle_cy = rect.y() + row_h / 2 + n_siblings = index.model().rowCount(index.parent()) + is_last = index.row() == n_siblings - 1 + pen = QPen(line_clr, self.line_width) pen.setCapStyle(Qt.PenCapStyle.RoundCap) painter.setPen(pen) painter.setBrush(Qt.GlobalColor.transparent) - path = QPainterPath() - # Start at the headers circle - path.moveTo(main_cx, header_cy) - # Line to first sub-step - path.lineTo(sub_tree_x, first_sub_cy) - # Line down to last sub-step - path.lineTo(sub_tree_x, last_sub_cy) - # Line back to main axis at the bottom - path.lineTo(main_cx - 0.3, bottom_y) - - painter.drawPath(path) - - # 3. Draw sub-step circles and text - for i, sub_step in enumerate(grouped_rewrites): - sub_cy = first_sub_cy + i * row_height - is_sub_selected = False - view = self.parent() - if isinstance(view, ProofStepView) and view.selected_sub_step is not None: - sel_step_idx, sel_sub_idx = view.selected_sub_step - if step_idx == sel_step_idx and i == sel_sub_idx: - is_sub_selected = True - - # Sub-step circle - painter.setPen(QPen(line_clr, self.line_width)) - if is_sub_selected: - painter.setBrush(display_setting.effective_colors["z_spider"]) # brighter blue when selected - r = self.circle_radius_selected - else: - painter.setBrush(display_setting.effective_colors["z_spider"]) # default steel-blue - r = self.circle_radius - painter.drawEllipse(QPointF(sub_tree_x, sub_cy), r, r) - - # Sub-step text - sub_text_x = int(sub_tree_x + self.circle_radius + 10) - sub_text_rect = QRect( - sub_text_x, - int(sub_cy - text_height / 2), - int(option.rect.width() - sub_text_x), # type: ignore[attr-defined] - text_height - ) - sub_font = QFont(font) - if is_sub_selected: - sub_font.setWeight(QFont.Weight.Bold) - painter.setFont(sub_font) - painter.setPen(fg) - painter.drawText(sub_text_rect, Qt.AlignmentFlag.AlignLeft, sub_step.display_name) - - def sizeHint(self, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> QSize: - size = super().sizeHint(option, index) - text_height = QFontMetrics(option.font).height() # type: ignore[attr-defined] - single_row = text_height + 2 * self.vert_padding - total = single_row - - is_grouped, is_expanded, grouped_rewrites = self._step_info(index) - if is_grouped and is_expanded and grouped_rewrites: - total += len(grouped_rewrites) * single_row + # Branch line: top → circle + painter.drawLine(QPointF(branch_x, rect.y()), QPointF(branch_x, circle_cy)) + # Branch line: circle → bottom (or diagonal back to main axis) + if is_last: + painter.drawLine(QPointF(branch_x, circle_cy), + QPointF(main_cx, rect.y() + rect.height())) + else: + painter.drawLine(QPointF(branch_x, circle_cy), + QPointF(branch_x, rect.y() + rect.height())) - return QSize(size.width(), total) + # Circle + painter.setPen(QPen(line_clr, self.line_width)) + painter.setBrush(display_setting.effective_colors["z_spider"]) + cr = self.circle_radius_selected \ + if option.state & QStyle.StateFlag.State_Selected else self.circle_radius # type: ignore[attr-defined] + painter.drawEllipse(QPointF(branch_x, circle_cy), cr, cr) + + # Text + sub_text_x = int(branch_x + self.circle_radius + 10) + draw_font = QFont(font) + if option.state & QStyle.StateFlag.State_Selected: # type: ignore[attr-defined] + draw_font.setWeight(QFont.Weight.Bold) + painter.setFont(draw_font) + painter.setPen(fg) + painter.drawText( + QRect(sub_text_x, int(circle_cy - text_h / 2), + int(rect.width() - sub_text_x), text_h), + Qt.AlignmentFlag.AlignLeft, + index.data(Qt.ItemDataRole.DisplayRole)) + + def sizeHint(self, option: QStyleOptionViewItem, + index: Union[QModelIndex, QPersistentModelIndex]) -> QSize: + size = super().sizeHint(option, index) + text_h = QFontMetrics(option.font).height() # type: ignore[attr-defined] + return QSize(size.width(), text_h + 2 * self.vert_padding) - def createEditor(self, parent: QWidget, option: QStyleOptionViewItem, index: Union[QModelIndex, QPersistentModelIndex]) -> QLineEdit: + def createEditor(self, parent: QWidget, option: QStyleOptionViewItem, + index: Union[QModelIndex, QPersistentModelIndex]) -> QLineEdit: return QLineEdit(parent) - def setEditorData(self, editor: QWidget, index: Union[QModelIndex, QPersistentModelIndex]) -> None: + def setEditorData(self, editor: QWidget, + index: Union[QModelIndex, QPersistentModelIndex]) -> None: assert isinstance(editor, QLineEdit) - value = index.model().data(index, Qt.ItemDataRole.DisplayRole) - editor.setText(str(value)) + editor.setText(str(index.model().data(index, Qt.ItemDataRole.DisplayRole))) - def setModelData(self, editor: QWidget, model: QAbstractItemModel, index: Union[QModelIndex, QPersistentModelIndex]) -> None: + def setModelData(self, editor: QWidget, model: QAbstractItemModel, + index: Union[QModelIndex, QPersistentModelIndex]) -> None: step_view = self.parent() assert isinstance(step_view, ProofStepView) assert isinstance(editor, QLineEdit) - step_view.rename_proof_step(editor.text(), index.row() - 1) + if index.parent().isValid(): + step_view.rename_proof_sub_step(editor.text(), index.parent().row() - 1, index.row()) + else: + step_view.rename_proof_step(editor.text(), index.row() - 1) From 284b5acaa606df795e570714d8de3d2b353842b5 Mon Sep 17 00:00:00 2001 From: axif Date: Thu, 5 Mar 2026 20:12:41 +0600 Subject: [PATCH 18/19] fix lint error --- zxlive/commands.py | 6 ++++-- zxlive/proof.py | 6 ++++-- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/zxlive/commands.py b/zxlive/commands.py index 5b983efd..df6c4661 100644 --- a/zxlive/commands.py +++ b/zxlive/commands.py @@ -445,7 +445,7 @@ class AddRewriteStep(UpdateGraph): The rewrite is inserted after the currently selected step. In particular, it replaces all rewrites that were previously after the current selection. """ - step_view: QListView + step_view: ProofStepView name: str diff: Optional[GraphDiff] = None @@ -556,7 +556,9 @@ class UngroupRewriteSteps(BaseCommand): _group_size: int = field(default=0, init=False) def redo(self) -> None: - self._group_size = len(self.step_view.model().steps[self.group_index].grouped_rewrites) + grouped = self.step_view.model().steps[self.group_index].grouped_rewrites + assert grouped is not None + self._group_size = len(grouped) self.step_view.model().ungroup_steps(self.group_index) self.step_view.move_to_step(self.group_index + 1) diff --git a/zxlive/proof.py b/zxlive/proof.py index 74057a9f..de15639b 100644 --- a/zxlive/proof.py +++ b/zxlive/proof.py @@ -81,7 +81,7 @@ def index(self, row: int, column: int, return self.createIndex(row, column, 0) return self.createIndex(row, column, parent.row() + 1) - def parent(self, child: Union[QModelIndex, QPersistentModelIndex]) -> QModelIndex: + def parent(self, child: Union[QModelIndex, QPersistentModelIndex]) -> QModelIndex: # type: ignore[override] if not child.isValid() or child.internalId() == 0: return QModelIndex() return self.createIndex(child.internalId() - 1, 0, 0) @@ -367,7 +367,9 @@ def proof_step_selected(self, selected: QItemSelection, deselected: QItemSelecti sub_idx = index.row() step = self.model().steps[step_idx] if step.grouped_rewrites and sub_idx < len(step.grouped_rewrites): - self.graph_view.set_graph(step.grouped_rewrites[sub_idx].graph.copy()) + graph = step.grouped_rewrites[sub_idx].graph.copy() + assert isinstance(graph, GraphT) + self.graph_view.set_graph(graph) else: self.graph_view.set_graph(self.model().get_graph(index.row())) From 9ed9fcf9b0ba891b63cc93f49b5bac452068d397 Mon Sep 17 00:00:00 2001 From: axif Date: Wed, 25 Mar 2026 16:19:48 +0600 Subject: [PATCH 19/19] remove unused QListView import --- zxlive/commands.py | 1 - 1 file changed, 1 deletion(-) diff --git a/zxlive/commands.py b/zxlive/commands.py index df6c4661..b7c75fa5 100644 --- a/zxlive/commands.py +++ b/zxlive/commands.py @@ -8,7 +8,6 @@ from PySide6.QtCore import QModelIndex from PySide6.QtGui import QUndoCommand -from PySide6.QtWidgets import QListView from pyzx.graph.diff import GraphDiff from pyzx.symbolic import Poly from pyzx.utils import EdgeType, VertexType, get_w_partner, vertex_is_w, get_w_io, get_z_box_label, set_z_box_label