adding universe encoding

This commit is contained in:
2023-08-23 09:47:19 +02:00
parent c3a4a1cd46
commit e5dd7194ba
3 changed files with 122 additions and 76 deletions

View File

@ -35,7 +35,7 @@
<header class="py-2 block text-white bg-neutral-900">
<div class="mx-auto flex flex-wrap pl-2 py-1 flex-row items-center">
<a class="flex title-font font-medium items-center text-black mb-0">
<svg xmlns="http://www.w3.org/2000/svg" fill="none" stroke="currentColor" stroke-linecap="round" stroke-linejoin="round" stroke-width="2" class="w-10 h-10 text-black p-2 bg-white rounded-full" viewBox="0 0 24 24">
<svg id="share_button" title="Share button" xmlns="http://www.w3.org/2000/svg" fill="none" stroke="currentColor" stroke-linecap="round" stroke-linejoin="round" stroke-width="2" class="w-10 h-10 text-black p-2 bg-white rounded-full" viewBox="0 0 24 24">
<path stroke-linecap="round" stroke-linejoin="round" d="M12 6.042A8.967 8.967 0 006 3.75c-1.052 0-2.062.18-3 .512v14.25A8.987 8.987 0 016 18c2.305 0 4.408.867 6 2.292m0-14.25a8.966 8.966 0 016-2.292c1.052 0 2.062.18 3 .512v14.25A8.987 8.987 0 0018 18a8.967 8.967 0 00-6 2.292m0-14.25v14.25" />
</svg>
<span id="universe-viewer" class="hidden xl:block ml-4 text-2xl text-white">Topos</span>

View File

@ -1,6 +1,6 @@
import { tutorial_universe } from "./universes/tutorial"
import { tutorial_universe } from "./universes/tutorial";
export type Universes = { [key: string]: Universe }
export type Universes = { [key: string]: Universe };
export interface Universe {
/**
@ -11,10 +11,10 @@ export interface Universe {
* @param init - Init file
* @param notes - Notes file
*/
global: File
locals: { [key: number]: File }
init: File
notes: File
global: File;
locals: { [key: number]: File };
init: File;
notes: File;
}
export interface File {
@ -25,9 +25,9 @@ export interface File {
* @param committed - The text that has been committed (e.g. stable)
* @param evaluations - The number of times the text has been evaluated
*/
candidate: string
committed?: string
evaluations?: number
candidate: string;
committed?: string;
evaluations?: number;
}
export interface Settings {
@ -42,13 +42,13 @@ export interface Settings {
* @param selected_universe - The name of the selected universe
* @param line_numbers - Whether or not to show line numbers
*/
vimMode: boolean
theme: string
font: string
font_size: number
universes: Universes
selected_universe: string
line_numbers: boolean
vimMode: boolean;
theme: string;
font: string;
font_size: number;
universes: Universes;
selected_universe: string;
line_numbers: boolean;
}
export const template_universe = {
@ -66,10 +66,10 @@ export const template_universe = {
},
init: { candidate: "", committed: "", evaluations: 0 },
notes: { candidate: "" },
}
};
export const template_universes = {
"Default": {
Default: {
global: { candidate: "", committed: "", evaluations: 0 },
locals: {
1: { candidate: "", committed: "", evaluations: 0 },
@ -85,12 +85,10 @@ export const template_universes = {
init: { candidate: "", committed: "", evaluations: 0 },
notes: { candidate: "// NOTES" },
},
"Help": tutorial_universe,
}
Help: tutorial_universe,
};
export class AppSettings {
/**
* AppSettings is a class that stores the settings for the Topos application.
* It is in charge of reading and writing to local storage and exposing that
@ -105,34 +103,37 @@ export class AppSettings {
* @param line_numbers - Whether or not to show line numbers
*/
public vimMode: boolean = false
public theme: string = "materialDark"
public font: string = "SpaceMono"
public font_size: number = 22
public universes: Universes
public selected_universe: string = "Default"
public line_numbers: boolean = true
public vimMode: boolean = false;
public theme: string = "materialDark";
public font: string = "SpaceMono";
public font_size: number = 22;
public universes: Universes;
public selected_universe: string = "Default";
public line_numbers: boolean = true;
constructor() {
const settingsFromStorage = JSON.parse(localStorage.getItem('topos') || "{}");
const settingsFromStorage = JSON.parse(
localStorage.getItem("topos") || "{}"
);
if (settingsFromStorage && Object.keys(settingsFromStorage).length !== 0) {
// let settings = JSON.parse(localStorage.getItem("topos") as string)
this.vimMode = settingsFromStorage.vimMode
this.theme = settingsFromStorage.theme
this.font = settingsFromStorage.font
this.font_size = settingsFromStorage.font_size
this.universes = settingsFromStorage.universes
this.selected_universe = settingsFromStorage.selected_universe
this.line_numbers = settingsFromStorage.line_numbers
this.vimMode = settingsFromStorage.vimMode;
this.theme = settingsFromStorage.theme;
this.font = settingsFromStorage.font;
this.font_size = settingsFromStorage.font_size;
this.universes = settingsFromStorage.universes;
this.selected_universe = settingsFromStorage.selected_universe;
this.line_numbers = settingsFromStorage.line_numbers;
} else {
this.universes = template_universes
this.universes = template_universes;
}
}
get_universe(universe_name: string) {
this.universes.universe_name;
}
get data(): Settings {
/**
* Returns the settings as a Settings object.
@ -144,11 +145,14 @@ export class AppSettings {
font_size: this.font_size,
universes: this.universes,
selected_universe: this.selected_universe,
line_numbers: this.line_numbers
}
line_numbers: this.line_numbers,
};
}
saveApplicationToLocalStorage(universes: Universes, settings: Settings): void{
saveApplicationToLocalStorage(
universes: Universes,
settings: Settings
): void {
/**
* Main method to store the application to local storage.
*
@ -161,6 +165,6 @@ export class AppSettings {
this.font_size = settings.font_size;
this.selected_universe = settings.selected_universe;
this.line_numbers = settings.line_numbers;
localStorage.setItem('topos', JSON.stringify(this.data))
localStorage.setItem("topos", JSON.stringify(this.data));
}
}

View File

@ -4,7 +4,7 @@ import { javascript } from "@codemirror/lang-javascript";
import { oneDark } from "@codemirror/theme-one-dark";
import { markdown } from "@codemirror/lang-markdown";
import { Extension, Prec } from "@codemirror/state";
import {indentWithTab} from "@codemirror/commands"
import { indentWithTab } from "@codemirror/commands";
import { vim } from "@replit/codemirror-vim";
import { AppSettings } from "./AppSettings";
import { editorSetup } from "./EditorSetup";
@ -164,6 +164,11 @@ export class Editor {
"vim-mode"
) as HTMLButtonElement;
// Share button
share_button: HTMLElement = document.getElementById(
"share_button"
) as HTMLElement;
// Error line
error_line: HTMLElement = document.getElementById(
"error_line"
@ -229,9 +234,16 @@ export class Editor {
...this.editorExtensions,
EditorView.lineWrapping,
dynamicPlugins.of(this.userPlugins),
Prec.highest(keymap.of([
{ key:"Ctrl-Enter", run: ()=>{return true} }
])),
Prec.highest(
keymap.of([
{
key: "Ctrl-Enter",
run: () => {
return true;
},
},
])
),
keymap.of([indentWithTab]),
],
doc: this.universes[this.selected_universe].locals[this.local_index]
@ -484,6 +496,20 @@ export class Editor {
this.settings.font_size = parseInt(new_value);
});
this.share_button.addEventListener("click", () => {
this.share_button.classList.add("animate-spin");
setInterval(
() => this.share_button.classList.remove("animate-spin"),
1000
);
// trigger a manual save
this.currentFile().candidate = app.view.state.doc.toString();
this.currentFile().committed = app.view.state.doc.toString();
this.settings.saveApplicationToLocalStorage(app.universes, app.settings);
// encode as a blob!
this.share();
});
this.normal_mode_button.addEventListener("click", () => {
this.settings.vimMode = false;
this.view.dispatch({ effects: this.vimModeCompartment.reconfigure([]) });
@ -564,6 +590,22 @@ export class Editor {
];
}
emptyUrl = () => {
window.history.replaceState({}, document.title, "/");
};
share() {
const hashed_table = JSON.stringify(
this.settings.universes[this.selected_universe]
);
const url = new URL(window.location.href);
url.searchParams.set(
"universe",
this.selected_universe + "-" + hashed_table
);
window.history.replaceState({}, "", url.toString());
}
showDocumentation() {
if (document.getElementById("app")?.classList.contains("hidden")) {
document.getElementById("app")?.classList.remove("hidden");