Operation history.
| 5673 | |
| 5674 | |
| 5675 | class History: |
| 5676 | """ |
| 5677 | Operation history. |
| 5678 | """ |
| 5679 | |
| 5680 | ops: list[Op] |
| 5681 | opDict: dict[str, Op] |
| 5682 | |
| 5683 | def __init__(self) -> None: |
| 5684 | |
| 5685 | self.ops = [] |
| 5686 | self.opDict = dict() |
| 5687 | |
| 5688 | def __getitem__(self, ix: int | str) -> Op: |
| 5689 | |
| 5690 | if isinstance(ix, str): |
| 5691 | return self.opDict[ix] |
| 5692 | else: |
| 5693 | return self.ops[ix] |
| 5694 | |
| 5695 | def pop(self) -> Op: |
| 5696 | |
| 5697 | return self.ops.pop() |
| 5698 | |
| 5699 | def append(self, op: Op, name: str | None = None) -> None: |
| 5700 | |
| 5701 | self.ops.append(op) |
| 5702 | if name: |
| 5703 | self.opDict[name] = op |
| 5704 | |
| 5705 | |
| 5706 | BuilderType: TypeAlias = ( |
no outgoing calls