add menu option for hovering tips

index.html

@@ -230,6 +230,10 @@
               	<div class="flex items-center mb-4 ml-8">
               	    <input id="show-time-position" type="checkbox" value="" class="w-4 h-4 text-blue-600 bg-gray-100 border-gray-300 rounded focus:ring-blue-500 dark:focus:ring-blue-600 dark:ring-offset-gray-800 focus:ring-2 dark:bg-gray-700 dark:border-gray-600">
               	    <label for="default-checkbox" class="ml-2 text-sm font-medium text-dark">Show Time Position</label>
+              	</div>
+              	<div class="flex items-center mb-4 ml-8">
+              	    <input id="show-tips" type="checkbox" value="" class="w-4 h-4 text-blue-600 bg-gray-100 border-gray-300 rounded focus:ring-blue-500 dark:focus:ring-blue-600 dark:ring-offset-gray-800 focus:ring-2 dark:bg-gray-700 dark:border-gray-600">
+              	    <label for="default-checkbox" class="ml-2 text-sm font-medium text-dark">Show Hovering Tips</label>
               	</div>
 							</div>
               <!-- Information card -->

src/AppSettings.ts

@@ -42,6 +42,8 @@ export interface Settings {
    * @param universes - The set universes to use (e.g. saved files)
    * @param selected_universe - The name of the selected universe
    * @param line_numbers - Whether or not to show line numbers
+   * @param time_position - Whether or not to show time position
+   * @param tips - Whether or not to show tips
    */
   vimMode: boolean;
   theme: string;
@@ -50,7 +52,8 @@ export interface Settings {
   universes: Universes;
   selected_universe: string;
   line_numbers: boolean;
-	time_position: boolean;
+  time_position: boolean;
+  tips: boolean;
 }
 
 export const template_universe = {
@@ -105,6 +108,9 @@ export class AppSettings {
    * @param universes - The set universes to use (e.g. saved files)
    * @param selected_universe - The name of the selected universe
    * @param line_numbers - Whether or not to show line numbers
+   * @param time_position - Whether or not to show time position
+   * @param tips - Whether or not to show tips
+
    */
 
   public vimMode: boolean = false;
@@ -114,7 +120,8 @@ export class AppSettings {
   public universes: Universes;
   public selected_universe: string = "Default";
   public line_numbers: boolean = true;
-	public time_position: boolean = true;
+  public time_position: boolean = true;
+  public tips: boolean = true;
 
   constructor() {
     const settingsFromStorage = JSON.parse(
@@ -131,6 +138,7 @@ export class AppSettings {
       this.selected_universe = settingsFromStorage.selected_universe;
       this.line_numbers = settingsFromStorage.line_numbers;
       this.time_position = settingsFromStorage.time_position;
+      this.tips = settingsFromStorage.tips;
     } else {
       this.universes = template_universes;
     }
@@ -152,7 +160,8 @@ export class AppSettings {
       universes: this.universes,
       selected_universe: this.selected_universe,
       line_numbers: this.line_numbers,
-			time_position: this.time_position
+      time_position: this.time_position,
+      tips: this.tips,
     };
   }
 
@@ -173,6 +182,7 @@ export class AppSettings {
     this.selected_universe = settings.selected_universe;
     this.line_numbers = settings.line_numbers;
     this.time_position = settings.time_position;
+    this.tips = settings.tips;
     localStorage.setItem("topos", JSON.stringify(this.data));
   }
 }

src/EditorSetup.ts

@@ -1,5 +1,3 @@
-import { inlineHoveringTips } from "./documentation/inlineHelp";
-
 import {
   keymap,
   highlightSpecialChars,
@@ -42,7 +40,6 @@ export const editorSetup: Extension = (() => [
   // crosshairCursor(),
   highlightActiveLine(),
   highlightSelectionMatches(),
-  inlineHoveringTips,
   keymap.of([
     ...closeBracketsKeymap,
     ...defaultKeymap,

src/main.ts

@@ -3,6 +3,7 @@ import { examples } from "./examples/excerpts";
 import { EditorState, Compartment } from "@codemirror/state";
 import { ViewUpdate, lineNumbers, keymap } from "@codemirror/view";
 import { javascript } from "@codemirror/lang-javascript";
+import { inlineHoveringTips } from "./documentation/inlineHelp";
 import { toposTheme } from "./themes/toposTheme";
 import { markdown } from "@codemirror/lang-markdown";
 import { Extension, Prec } from "@codemirror/state";
@@ -72,6 +73,7 @@ export class Editor {
   fontSize: Compartment;
   withLineNumbers: Compartment;
   vimModeCompartment: Compartment;
+  hoveringCompartment: Compartment;
   chosenLanguage: Compartment;
   currentDocumentationPane: string = "introduction";
   exampleCounter: number = 0;
@@ -185,6 +187,10 @@ export class Editor {
     "show-time-position"
   ) as HTMLInputElement;
 
+  // Hovering tips checkbox
+  tips_checkbox: HTMLInputElement = document.getElementById(
+    "show-tips"
+  ) as HTMLInputElement;
 
   // Editor mode selection
   normal_mode_button: HTMLButtonElement = document.getElementById(
@@ -231,12 +237,12 @@ export class Editor {
     this.universes[this.selected_universe].global.committed = random_example;
     this.universes[this.selected_universe].global.candidate = random_example;
 
-		this.line_numbers_checkbox.checked = this.settings.line_numbers;
+    this.line_numbers_checkbox.checked = this.settings.line_numbers;
-		this.time_position_checkbox.checked = this.settings.time_position;
+    this.time_position_checkbox.checked = this.settings.time_position;
-		if (!this.settings.time_position) {
+    this.tips_checkbox.checked = this.settings.tips;
-			document.getElementById('timeviewer')!.classList.add('hidden');
+    if (!this.settings.time_position) {
-		}
+      document.getElementById("timeviewer")!.classList.add("hidden");
-
+    }
 
     // ================================================================================
     // Audio context and clock
@@ -258,6 +264,7 @@ export class Editor {
     // ================================================================================
 
     this.vimModeCompartment = new Compartment();
+    this.hoveringCompartment = new Compartment();
     this.withLineNumbers = new Compartment();
     this.chosenLanguage = new Compartment();
     this.fontSize = new Compartment();
@@ -280,6 +287,7 @@ export class Editor {
       this.withLineNumbers.of(lines),
       this.fontSize.of(fontModif),
       this.vimModeCompartment.of(vimPlugin),
+      this.hoveringCompartment.of(this.settings.tips ? inlineHoveringTips : []),
       editorSetup,
       toposTheme,
       this.chosenLanguage.of(javascript()),
@@ -537,6 +545,7 @@ export class Editor {
       );
       this.line_numbers_checkbox.checked = this.settings.line_numbers;
       this.time_position_checkbox.checked = this.settings.time_position;
+      this.tips_checkbox.checked = this.settings.tips;
       let modal_settings = document.getElementById("modal-settings");
       let editor = document.getElementById("editor");
       modal_settings?.classList.remove("invisible");
@@ -595,12 +604,23 @@ export class Editor {
       });
     });
 
-
     this.time_position_checkbox.addEventListener("change", () => {
-			let timeviewer = document.getElementById("timeviewer") as HTMLElement;
+      let timeviewer = document.getElementById("timeviewer") as HTMLElement;
       let checked = this.time_position_checkbox.checked ? true : false;
       this.settings.time_position = checked;
-			checked ? timeviewer.classList.remove('hidden') : timeviewer.classList.add('hidden');
+      checked
+        ? timeviewer.classList.remove("hidden")
+        : timeviewer.classList.add("hidden");
+    });
+
+    this.tips_checkbox.addEventListener("change", () => {
+      let checked = this.tips_checkbox.checked ? true : false;
+      this.settings.tips = checked;
+      this.view.dispatch({
+        effects: this.hoveringCompartment.reconfigure(
+          checked ? inlineHoveringTips : []
+        ),
+      });
     });
 
     this.vim_mode_button.addEventListener("click", () => {