Skip to content

Commit ace69d9

Browse files
committed
set lean4.infoview.showGoalNames and lean4.infoview.emphasizeFirstGoal
1 parent ea8f144 commit ace69d9

File tree

2 files changed

+5
-3
lines changed

2 files changed

+5
-3
lines changed

client/src/App.tsx

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -157,6 +157,8 @@ function App() {
157157
"editor.semanticHighlighting.enabled": true,
158158
"editor.acceptSuggestionOnEnter": preferences.acceptSuggestionOnEnter ? "on" : "off",
159159
"lean4.input.eagerReplacementEnabled": true,
160+
"lean4.infoview.showGoalNames": false,
161+
"lean4.infoview.emphasizeFirstGoal": true,
160162
"lean4.input.leader": preferences.abbreviationCharacter
161163
}
162164
}

package-lock.json

Lines changed: 3 additions & 3 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)