Add ability to rename proof steps

Doubling clicking on the proof step will open a dialog prompting a new
name for the proof step.

A separate display name attribute was added to the Rewrite class rather
than modifying the "rule" attribute since "rule" is used when converting
a proof to a tikz diagram.

Fixes #189.

zxlive/commands.py

@@ -47,6 +47,18 @@ def update_graph_view(self, select_new: bool = False) -> None:
         #  we could store "dirty flags" for each node/edge.
         self.graph_view.update_graph(self.g, select_new)
 
+@dataclass
+class UndoableChange(BaseCommand):
+    """ Generic undoable change in the graph that can be appended to the
+    undo stack
+
+    Can be initialised as: UndoableChange(<parent>, <undo_cmd>, <redo_cmd>)
+
+    Where <parent> must contain the graph_view attribute as it is used in
+    BaseCommand.
+    """
+    undo: Callable[[], None]
+    redo: Callable[[], None]
 
 @dataclass
 class SetGraph(BaseCommand):
@@ -370,7 +382,7 @@ def redo(self) -> None:
             self._old_steps.append(self.proof_model.pop_rewrite())
 
         diff = self.diff or GraphDiff(self.g, self.new_g)
-        self.proof_model.add_rewrite(Rewrite(self.name, diff), self.new_g)
+        self.proof_model.add_rewrite(Rewrite(self.name, self.name, diff), self.new_g)
 
         # Select the added step
         idx = self.step_view.model().index(self.proof_model.rowCount() - 1, 0, QModelIndex())

zxlive/proof.py

@@ -1,7 +1,8 @@
 import json
 from typing import NamedTuple, Union, Any
 
-from PySide6.QtCore import QAbstractListModel, QModelIndex, QPersistentModelIndex, Qt
+from PySide6.QtCore import (QAbstractListModel, QModelIndex, QPersistentModelIndex,
+                            Qt, QAbstractItemModel)
 from PySide6.QtGui import QFont
 from pyzx.graph import GraphDiff
 
@@ -11,12 +12,14 @@
 class Rewrite(NamedTuple):
     """A rewrite turns a graph into another graph."""
 
+    display_name: str # Name of proof displayed to user
     rule: str  # Name of the rule that was applied to get to this step
     diff: GraphDiff  # Diff from the last step to this step
 
     def to_json(self) -> str:
         """Serializes the rewrite to JSON."""
         return json.dumps({
+            "display_name": self.display_name,
             "rule": self.rule,
             "diff": self.diff.to_json()
         })
@@ -25,7 +28,9 @@ def to_json(self) -> str:
     def from_json(json_str: str) -> "Rewrite":
         """Deserializes the rewrite from JSON."""
         d = json.loads(json_str)
+
         return Rewrite(
+            display_name=d.get("display_name", d["rule"]), # Old proofs may not have display names
             rule=d["rule"],
             diff=GraphDiff.from_json(d["diff"])
         )
@@ -66,7 +71,7 @@ def data(self, index: Union[QModelIndex, QPersistentModelIndex], role: int=Qt.It
             if index.row() == 0:
                 return "START"
             else:
-                return self.steps[index.row()-1].rule
+                return self.steps[index.row()-1].display_name
         elif role == Qt.ItemDataRole.FontRole:
             return QFont("monospace", 12)
 
@@ -117,6 +122,19 @@ def get_graph(self, index: int) -> GraphT:
         assert isinstance(copy, GraphT)  # type: ignore
         return copy
 
+    def rename_step(self, index: int, name: str):
+        """Change the display name"""
+        old_step = self.steps[index]
+
+        # 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.diff)
+
+        # Rerender the proof step otherwise it will display the old name until
+        # the cursor moves
+        modelIndex = self.createIndex(index, 0)
+        self.dataChanged.emit(modelIndex, modelIndex, [])
+
     def to_json(self) -> str:
         """Serializes the model to JSON."""
         initial_graph_tikz = self.graphs[0].to_json()

zxlive/proof_panel.py

@@ -65,9 +65,27 @@ def __init__(self, graph: GraphT, *actions: QAction) -> None:
         self.step_view.setCurrentIndex(self.proof_model.index(0, 0))
         self.step_view.selectionModel().selectionChanged.connect(self._proof_step_selected)
         self.step_view.viewport().setAttribute(Qt.WidgetAttribute.WA_Hover)
+        self.step_view.doubleClicked.connect(self.__doubleClickHandler)
 
         self.splitter.addWidget(self.step_view)
 
+    def __doubleClickHandler(self, index: QModelIndex | QPersistentModelIndex):
+        # The first row in the item list is the START step, which is not interactive
+        if index.row() == 0:
+            return
+
+        new_name, ok = QInputDialog.getText(self, "Rename proof step", "Enter new name")
+
+        if ok:
+            # Subtract 1 from index since the START step isn't part of the model
+            old_name = self.proof_model.steps[index.row()-1].display_name
+            cmd = UndoableChange(self,
+                lambda: self.proof_model.rename_step(index.row()-1, old_name),
+                lambda: self.proof_model.rename_step(index.row()-1, new_name)
+            )
+
+            self.undo_stack.push(cmd)
+
     def _toolbar_sections(self) -> Iterator[ToolbarSection]:
         icon_size = QSize(32, 32)
         self.selection = QToolButton(self)