Merge pull request #364 from zxcalc/bug/saving-proofs-broken

Fix loading proofs is broken

zxlive/base_panel.py

@@ -54,12 +54,14 @@ def __init__(self, *actions: QAction) -> None:
 
         # Use box layout that fills the entire tab
         self.setLayout(QVBoxLayout())
-        self.layout().setSpacing(0)
+        layout = self.layout()
+        assert layout is not None # for mypy
+        layout.setSpacing(0)
         self.toolbar = QToolBar()
-        self.layout().addWidget(self.toolbar)
+        layout.addWidget(self.toolbar)
 
         self.splitter = QSplitter(self)
-        self.layout().addWidget(self.splitter)
+        layout.addWidget(self.splitter)
         self.splitter.splitterMoved.connect(self.sync_splitter_sizes)
 
         self.file_path = None

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/editor_base_panel.py

@@ -327,6 +327,7 @@ def add_item(self, name: str) -> None:
             combobox.setCurrentIndex(0)
         combobox.currentTextChanged.connect(lambda text: self._text_changed(name, text))
         item = self._layout.itemAtPosition(2 + self._items, 2)
+        assert item is not None # For mypy
         self._layout.removeItem(item)
         self._layout.addWidget(QLabel(f"<pre>{name}</pre>"), 2 + self._items, 0, Qt.AlignmentFlag.AlignVCenter | Qt.AlignmentFlag.AlignRight)
         self._layout.addWidget(combobox, 2 + self._items, 2, Qt.AlignmentFlag.AlignCenter)

zxlive/mainwindow.py

@@ -63,8 +63,10 @@ def __init__(self) -> None:
         w = QWidget(self)
         w.setLayout(QVBoxLayout())
         self.setCentralWidget(w)
-        w.layout().setContentsMargins(0, 0, 0, 0)
-        w.layout().setSpacing(0)
+        wlayout = w.layout()
+        assert wlayout is not None # for mypy
+        wlayout.setContentsMargins(0, 0, 0, 0)
+        wlayout.setSpacing(0)
         self.resize(1200, 800)
 
         # restore the window from the last time it was opened
@@ -74,7 +76,7 @@ def __init__(self) -> None:
         self.show()
 
         tab_widget = QTabWidget(self)
-        w.layout().addWidget(tab_widget)
+        wlayout.addWidget(tab_widget)
         tab_widget.setTabsClosable(True)
         tab_widget.currentChanged.connect(self.tab_changed)
         tab_widget.tabCloseRequested.connect(self.close_tab)
@@ -315,8 +317,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:
@@ -340,7 +341,7 @@ def close_tab(self, i: int) -> bool:
             name = self.tab_widget.tabText(i).replace("*","")
             answer = QMessageBox.question(self, "Save Changes",
                             f"Do you wish to save your changes to {name} before closing?",
-                            QMessageBox.StandardButton.Yes | QMessageBox.StandardButton.No | QMessageBox.StandardButton.Cancel)
+                            QMessageBox.StandardButton.Yes | QMessageBox.StandardButton.No | QMessageBox.StandardButton.Cancel) # type: ignore
             if answer == QMessageBox.StandardButton.Cancel:
                 return False
             if answer == QMessageBox.StandardButton.Yes:
@@ -585,7 +586,7 @@ def format_str(c: complex) -> str:
         table.resizeColumnsToContents()
         table.resizeRowsToContents()
         dialog.setLayout(QVBoxLayout())
-        dialog.layout().addWidget(table)
+        dialog.layout().addWidget(table) # type: ignore # mypy thinks this can be None
         dialog.exec()
 
     def proof_as_lemma(self) -> None:

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()

zxlive/vitem.py

@@ -307,7 +307,7 @@ def mouseReleaseEvent(self, e: QGraphicsSceneMouseEvent) -> None:
             e.ignore()
             return
         if e.button() == Qt.MouseButton.LeftButton:
-            if self._old_pos != self.pos():
+            if self._old_pos is None or self._old_pos != self.pos():
                 if self.ty == VertexType.W_INPUT:
                     # set the position of w_in to next to w_out at the same angle
                     w_out = get_w_partner_vitem(self)