diff --git a/index.html b/index.html
index 53d0141..54167a1 100644
--- a/index.html
+++ b/index.html
@@ -230,6 +230,10 @@
+
+
+
+
diff --git a/src/AppSettings.ts b/src/AppSettings.ts
index 9a2d483..3cd2908 100644
--- a/src/AppSettings.ts
+++ b/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));
}
}
diff --git a/src/EditorSetup.ts b/src/EditorSetup.ts
index 28f73b9..b2a50ba 100644
--- a/src/EditorSetup.ts
+++ b/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,
diff --git a/src/main.ts b/src/main.ts
index 57d71a9..dd7fbcc 100644
--- a/src/main.ts
+++ b/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.time_position_checkbox.checked = this.settings.time_position;
- if (!this.settings.time_position) {
- document.getElementById('timeviewer')!.classList.add('hidden');
- }
-
+ 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;
+ 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", () => {