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

@@ -370,7 +370,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

@@ -11,12 +11,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 +27,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 +70,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 +121,14 @@ 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)
+
     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,22 @@ 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 is the START step which can't be renamed
+        if index.row() == 0:
+            return
+
+        new_name, ok = QInputDialog.getText(
+            self, "Rename proof step", "Enter display name of proof step"
+        )
+        if ok:
+            # Subtract 1 from index since the START step isn't part of the model
+            index.model().rename_step(index.row()-1, new_name)
+
     def _toolbar_sections(self) -> Iterator[ToolbarSection]:
         icon_size = QSize(32, 32)
         self.selection = QToolButton(self)