Keyboard shortcuts are read on every focused tab.

[MacroLens]

When you create two separate proof tabs you can use shortcut keys on them simultaneously. I.e. append new proof lines to both proofs. This is unintended behavior.

Steps to recreate:

1. Start Aris
2. Click on any proof line to focus it.
3. Click on resolution_example.bram.
4. Click on any proof line to focus it.
5. Activate a keyboard shortcut, i.e. Ctrl-a

Possible Solution: Don't register key events for every ProofWidget. Register key events at either the app level or the TabbedContainer level. Send those event actions down to the focused tab.

[MacroLens]

Additionally, it looks like if you delete a line, the document becomes unfocused. So key events aren't handled and thus allow the user to use standard shortcuts from the browser.

[io12]

it looks like if you delete a line, the document becomes unfocused

It's been a long time since I worked on Aris, but I remember it used to be like this (before https://github.com/Bram-Hub/aris/commit/d575db66d3426146cebb5b16ab50c68000714399) but was hard to implement safely. The comment added in that commit has more context.

[MacroLens]

I remember reading that when I was applying a solution for b2d7ebe. Is there any particular reason why key handling was done at the proof level and not the application level?

[io12]

I don't remember. It may have just been the easiest at the time. I think you're right that application level is the better place for key handling though.