From e392367f21e26ed5bd1bb3ff7191c8cb4306d9f7 Mon Sep 17 00:00:00 2001
From: MohammadYusif <MohammadYusif@users.noreply.github.com>
Date: Fri, 19 Jun 2026 22:21:42 +0300
Subject: [PATCH] fix: respect infoview display settings for goals in messages
 (#734)

Goals embedded in messages (e.g. the "unsolved goals" diagnostic) were
rendered by InteractiveMessageTag in traceExplorer.tsx with a hardcoded
settings object, so user infoview settings such as "Display target before
assumptions" (reverseTacticState) were ignored for these goals.

Derive the settings from ConfigContext via the existing
goalSettingsStateOfConfig helper (now exported from goals.tsx), so
message-embedded goals respect the same display settings as the main
goal panel.
---
 lean4-infoview/src/infoview/goals.tsx         |  2 +-
 lean4-infoview/src/infoview/traceExplorer.tsx | 20 ++++---------------
 2 files changed, 5 insertions(+), 17 deletions(-)

diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx
index 78d42d56..afd95883 100644
--- a/lean4-infoview/src/infoview/goals.tsx
+++ b/lean4-infoview/src/infoview/goals.tsx
@@ -64,7 +64,7 @@ interface GoalSettingsState {
     showLetValue: boolean
 }
 
-function goalSettingsStateOfConfig(config: InfoviewConfig): GoalSettingsState {
+export function goalSettingsStateOfConfig(config: InfoviewConfig): GoalSettingsState {
     return {
         reverse: config.reverseTacticState,
         hideGoalNames: !config.showGoalNames,
diff --git a/lean4-infoview/src/infoview/traceExplorer.tsx b/lean4-infoview/src/infoview/traceExplorer.tsx
index 51b7e65c..8bf478f0 100644
--- a/lean4-infoview/src/infoview/traceExplorer.tsx
+++ b/lean4-infoview/src/infoview/traceExplorer.tsx
@@ -9,7 +9,8 @@
 
 import { HighlightedMsgEmbed, HighlightedTraceEmbed, lazyTraceChildrenToInteractive } from '@leanprover/infoview-api'
 import * as React from 'react'
-import { Goal } from './goals'
+import { ConfigContext } from './contexts'
+import { Goal, goalSettingsStateOfConfig } from './goals'
 import {
     InteractiveCode,
     InteractiveTaggedText,
@@ -117,26 +118,13 @@ function Trace(traceEmbed: HighlightedTraceEmbed) {
 function InteractiveMessageTag({
     tag: embed,
 }: InteractiveTagProps<HighlightedMsgEmbed, HighlightedMsgEmbed>): JSX.Element {
+    const config = React.useContext(ConfigContext)
     if (embed === 'highlighted') {
         return <span className="highlighted-text"></span>
     }
     if ('expr' in embed) return <InteractiveCode fmt={embed.expr} />
     else if ('goal' in embed)
-        return (
-            <Goal
-                goal={embed.goal}
-                settings={{
-                    reverse: false,
-                    hideGoalNames: false,
-                    emphasizeFirstGoal: false,
-                    showType: true,
-                    showInstance: true,
-                    showHiddenAssumption: true,
-                    showLetValue: true,
-                }}
-                additionalClassNames=""
-            />
-        )
+        return <Goal goal={embed.goal} settings={goalSettingsStateOfConfig(config)} additionalClassNames="" />
     else if ('widget' in embed)
         return <DynamicComponent hash={embed.widget.wi.javascriptHash} props={embed.widget.wi.props} />
     else if ('trace' in embed) return <Trace {...embed.trace} />