Loading a proof into ZXLive didn't allow you to go back to previous s…

…teps. This is now fixed.

zxlive/custom_rule.py

@@ -183,7 +183,8 @@ def from_json(cls, json_str: Union[str,Dict[str,Any]]) -> "CustomRule":
         lhs_graph = GraphT.from_json(d['lhs_graph'])
         rhs_graph = GraphT.from_json(d['rhs_graph'])
         # Mypy issue: https://github.com/python/mypy/issues/11673
-        assert (isinstance(lhs_graph, GraphT) and isinstance(rhs_graph, GraphT))  # type: ignore
+        if TYPE_CHECKING:
+            assert (isinstance(lhs_graph, GraphT) and isinstance(rhs_graph, GraphT))  # type: ignore
         lhs_graph.set_auto_simplify(False)
         rhs_graph.set_auto_simplify(False)
         return cls(lhs_graph, rhs_graph, d['name'], d['description'])

zxlive/mainwindow.py

@@ -315,8 +315,7 @@ def _open_file_from_output(self, out: ImportGraphOutput | ImportProofOutput | Im
                 self.new_deriv(graph, name)
                 assert isinstance(self.active_panel, ProofPanel)
                 proof_panel: ProofPanel = self.active_panel
-                proof_panel.step_view.setModel(out.p)
-                proof_panel.step_view.setCurrentIndex(proof_panel.proof_model.index(len(proof_panel.proof_model.steps), 0))
+                proof_panel.step_view.set_model(out.p)
             elif isinstance(out, ImportRuleOutput):
                 self.new_rule_editor(out.r, name)
             else:

zxlive/proof.py

@@ -226,6 +226,7 @@ class ProofStepView(QListView):
     """A view for displaying the steps in a proof."""
 
     def __init__(self, parent: 'ProofPanel'):
+        print("Initializing ProofStepView")
         super().__init__(parent)
         self.graph_view = parent.graph_view
         self.undo_stack = parent.undo_stack
@@ -251,14 +252,23 @@ def model(self) -> ProofModel:
         assert isinstance(model, ProofModel)
         return model
 
+    def set_model(self, model: ProofModel) -> None:
+        self.setModel(model)
+        # 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 move_to_step(self, index: int) -> None:
+        print("Moving to step", index)
         idx = self.model().index(index, 0, QModelIndex())
         self.clearSelection()
         self.selectionModel().blockSignals(True)
         self.setCurrentIndex(idx)
         self.selectionModel().blockSignals(False)
         self.update(idx)
-        self.graph_view.set_graph(self.model().get_graph(index))
+        g = self.model().get_graph(index)
+        print(g)
+        self.graph_view.set_graph(g)
 
     def show_context_menu(self, position: QPoint) -> None:
         selected_indexes = self.selectedIndexes()