EDITOR: changed editor tabs to have their own editor mode (#1372)

This commit is contained in:
G4mingJon4s
2024-06-13 04:19:40 +02:00
committed by GitHub
parent 805ca06922
commit bec6e82d7f
11 changed files with 34 additions and 18 deletions
+2 -1
View File
@@ -72,6 +72,7 @@ import { MathJaxContext } from "better-react-mathjax";
import { useRerender } from "./React/hooks";
import { HistoryProvider } from "./React/Documentation";
import { GoRoot } from "../Go/ui/GoRoot";
import { Settings } from "../Settings/Settings";
import { isBitNodeFinished } from "../BitNode/BitNodeUtils";
const htmlLocation = location;
@@ -252,7 +253,7 @@ export function GameRoot(): React.ReactElement {
<ScriptEditorRoot
files={pageWithContext.files ?? new Map()}
hostname={pageWithContext.options?.hostname ?? Player.getCurrentServer().hostname}
vim={!!pageWithContext.options?.vim}
vim={pageWithContext.options === undefined ? Settings.MonacoDefaultToVim : pageWithContext.options.vim}
/>
);
break;
+1 -1
View File
@@ -89,7 +89,7 @@ export type PageWithContext =
| { page: SimplePage };
export interface ScriptEditorRouteOptions {
vim?: boolean;
vim: boolean;
hostname?: string;
}