Method collect_sorrys

lean_py/kernel.py:388–393

Extract all `sorry` placeholders in ``source`` as a draftable :class:`GoalState`. Returns ``(state, message)`` — state is ``None`` if no sorries were found.

(self, source: str)

        return self._lib.leanpy_kernel_frontend_process(source)

    def collect_sorrys(self, source: str) -> tuple[GoalState | None, str]:
        """Extract all `sorry` placeholders in ``source`` as a draftable
        :class:`GoalState`. Returns ``(state, message)`` — state is ``None`` if
        no sorries were found."""
        handle, msg = self._lib.leanpy_kernel_frontend_collect_sorrys(source)
        return (GoalState(self, handle) if handle is not None else None, msg)

    # -- delab utilities -------------------------------------------------