Agda 2.9.0 release candidate 3 (including tests) - #8891

Closes #8858

<details>
<summary>Claudesplanation</summary>

I implemented the suggested fix: after Give or Refine, `Cmd_highlight` no longer emits stale annotations. I confirmed the bug on an older binary (`agda-8811`, from early October), and the new test shows it gone with the patched build.

**Is the suggested fix reasonable?** Yes. The entries `give_gen` records in `stDisambiguatedNames` carry ranges inside the old goal. They are only correct for the highlighting `give_gen` does right away, while the text is still inside the goal. Once the goal is replaced by the expression, they point at the wrong place. A fresh reload starts with an empty map, so dropping them loses nothing that a reload would have. The issue's fallback options (removing entries by range, or skipping `generateConstructorInfo` in `Cmd_highlight`) only treat the symptom.

**The change** is in `give_gen` in `src/full/Agda/Interaction/InteractionTop.hs`:
```haskell
disambiguatedNames <- useTC stDisambiguatedNames
flip finally (setTCLens stDisambiguatedNames disambiguatedNames) $ unless (null s) $ do ...
```
- The map is saved on entry and restored at the end, after the immediate highlighting has used it. Every other state change Give or Refine makes is kept.
- `finally` also restores the map when the give fails with an error, so a failed attempt doesn't leave entries behind either.

**Test:** I added `test/Interaction/Issue8858.{agda,sh,out}`, which runs both reproductions from the issue in one file:
- **Give:** `con x y` on an ambiguous constructor. The old binary reports `x` as a constructor with `con`'s definition site; now `con` is a constructor and `x`, `y` are `bound`.
- **Refine:** a record expression. The old binary returns `(103 105 (field)) (105 106 …) (106 108 …)`; now it returns just `(103 106 (field)) (113 116 (field))`.

</summary>

Repeatedly dividing even numbers by 2 might just not terminate.  That pesky 0.

Fixed manually.

Closes #8898.