add showGoalNames to the settings

Author: joneugster

client/src/App.tsx

@@ -157,7 +157,7 @@ function App() {
         "editor.semanticHighlighting.enabled": true,
         "editor.acceptSuggestionOnEnter": preferences.acceptSuggestionOnEnter ? "on" : "off",
         "lean4.input.eagerReplacementEnabled": true,
-        "lean4.infoview.showGoalNames": false,
+        "lean4.infoview.showGoalNames": preferences.showGoalNames,
         "lean4.infoview.emphasizeFirstGoal": true,
         "lean4.infoview.showExpectedType": false,
         "lean4.infoview.showTooltipOnHover": false,

client/src/Popups/Settings.tsx

@@ -87,6 +87,11 @@ const SettingsPopup: FC<{
         checked={preferences.acceptSuggestionOnEnter} />
         <label htmlFor="acceptSuggestionOnEnter">Accept Suggestion on Enter</label>
       </p>
+      <p>
+        <Switch id="showGoalNames" onChange={() => {modifyPreferences("showGoalNames", !preferences.showGoalNames)}}
+        checked={preferences.showGoalNames} />
+        <label htmlFor="showGoalNames">Show Goal Names</label>
+      </p>
 
       <h2>User settings</h2>
       <p>

client/src/config/settings.ts

@@ -10,6 +10,7 @@ Note that more Editor options are set in `App.tsx` directly.
 export interface IPreferencesContext {
   abbreviationCharacter: string
   acceptSuggestionOnEnter: boolean
+  showGoalNames: boolean
   compress: boolean, // compress the `code=` in the URL into `codez=` using LZ-string
   mobile: boolean
   saveInLocalStore: boolean
@@ -21,6 +22,7 @@ export interface IPreferencesContext {
 const settings: IPreferencesContext = {
   abbreviationCharacter: '\\',
   acceptSuggestionOnEnter: false,
+  showGoalNames: true,
   compress: true,
   mobile: false, // value irrelevant as it will be overwritten with `width < 800` in App.tsx
   saveInLocalStore: false, // should be false unless user gave consent.