Function focus 

pub fn focus(t: Tactic) -> Tactic

· t / focus t / next t: run t on the focused goal ALONE, and make it an error for the block to leave that goal open.

A script is otherwise a flat list of chains, and because subgoals are pushed to the front, stripping Lean’s bullets and concatenating the blocks WORKS — right up until a block leaves a goal open or closes two, at which point the blocks silently misalign and, with generic enough tactics, the proof still succeeds having proved the goals in a pairing the source never specified. The bullet is what makes that impossible, so it is the ERROR, not the focusing, that is the capability here.