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} />