BuboBubo/topos
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

slow and tedious progress

Browse Source
This commit is contained in:
Raphaël Forment
2023-12-15 16:56:54 +01:00
parent 32ae67b2c6
commit fb4d311ba8
4 changed files with 60 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files

27
src/main.ts
View File

@ -34,6 +34,7 @@ import { makeNumberExtensions } from "./extensions/NumberExtensions";
// @ts-ignore
import { registerSW } from "virtual:pwa-register";
import colors from "./colors.json";
import { code } from "./documentation/basics/code";
if ("serviceWorker" in navigator) {
registerSW();
@ -53,6 +54,7 @@ export class Editor {
hidden_interface: boolean = false;
fontSize!: Compartment;
withLineNumbers!: Compartment;
themeCompartment!: Compartment;
vimModeCompartment!: Compartment;
hoveringCompartment!: Compartment;
completionsCompartment!: Compartment;
@ -207,6 +209,9 @@ export class Editor {
// Loading universe from URL (if needed)
loadUniverserFromUrl(this);
// Set the color scheme for the application
this.readTheme("Floraverse");
}
private getBuffer(type: string): any {
@ -294,9 +299,9 @@ export class Editor {
*/
const tabs = document.querySelectorAll('[id^="tab-"]');
const tab = tabs[i] as HTMLElement;
tab.classList.add("bg-orange-300");
tab.classList.add("bg-color3");
for (let j = 0; j < tabs.length; j++) {
if (j != i) tabs[j].classList.remove("bg-orange-300");
if (j != i) tabs[j].classList.remove("bg-color3");
}
let tab_id = tab.id.split("-")[1];
this.local_index = parseInt(tab_id);
@ -319,15 +324,15 @@ export class Editor {
let changeColor = (button: HTMLElement) => {
interface_buttons.forEach((button) => {
let svg = button.children[0] as HTMLElement;
if (svg.classList.contains("text-orange-300")) {
svg.classList.remove("text-orange-300");
button.classList.remove("text-orange-300");
if (svg.classList.contains("text-color3")) {
svg.classList.remove("text-color3");
button.classList.remove("text-color3");
}
});
button.children[0].classList.remove("text-white");
button.children[0].classList.add("text-orange-300");
button.classList.add("text-orange-300");
button.classList.add("fill-orange-300");
button.children[0].classList.add("text-color3");
button.classList.add("text-color3");
button.classList.add("fill-color3");
};
switch (mode) {
@ -442,7 +447,7 @@ export class Editor {
unfocusPlayButtons() {
document.querySelectorAll('[id^="play-button-"]').forEach((button) => {
button.children[0].classList.remove("fill-orange-300");
button.children[0].classList.remove("fill-color3");
button.children[0].classList.remove("animate-pulse");
});
}
@ -591,6 +596,10 @@ export class Editor {
if (selected_theme) {
this.updateInterfaceTheme(selected_theme);
let codeMirrorTheme = getCodeMirrorTheme(selected_theme);
// Reconfigure the view with the new theme
this.view.dispatch({
effects: this.themeCompartment.reconfigure(codeMirrorTheme),
});
}
}
}