fix: ensure incremental commands and tactics are reached only on supported paths

[Kha]

Without this, it would not easy but perhaps be feasible to break incrementality when editing command prefixes such as set_option ... in theorem or also theorem namesp.name ... (which is a macro), especially if at some later point we support incrementality in input shifted by an edit. Explicit, sound support for these common cases will be brought back soon.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 67338bac2333fa39a8656e8f90574784e4c23d3d --onto d984030c6a683a80313917b6fd3e77abdf497809. (2024-05-23 18:00:04)