Display target before assumptions not always respected

[MoritzBeroRoos]

Description

There are situations (e.g. in messages) where the Infoview setting Display target before assumptions is not respected.
E.g. click on the underscore in the following:

theorem bla (a : False) : 1 = 2 := by sorry

theorem bla2 : 1 = 2 := by
  let := 1
  rw [bla (by _)]

The infoview shows the message

unsolved goals
this : Nat := 1
⊢ False

although i have set the setting to true.
This makes for a lot of scrolling in proofs with large contextes before i can finally see the goal.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[MohammadYusif]

I traced this to the infoview's message renderer: in lean4-infoview/src/infoview/traceExplorer.tsx, goals embedded in messages (like the "unsolved goals" diagnostic) are rendered with a hardcoded settings object (reverse: false, etc.) instead of the user's infoview configuration, so Display target before assumptions (and the other display toggles) are ignored there. I'm planning to fix it by deriving those settings from ConfigContext via the existing goalSettingsStateOfConfig helper that the main goal panel already uses, so message-embedded goals respect the same settings. Happy to discuss if there's a preferred direction before I open a PR.