user interface improvement

This commit is contained in:
2023-09-07 18:07:53 +02:00
parent 281c630827
commit 3a6c6f7a10

View File

@ -231,6 +231,13 @@ 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');
}
// ================================================================================
// Audio context and clock
// ================================================================================