Switch notebook editors to monaco (#239)

* Upgrade nteract packages and related dependencies to make new stateful-component work

* Switch to new monacoEditor

* Configure store using nteract mythic configuration

* Replace CodeMirror with Monaco editor in NotebookReadOnlyRenderer

* Reformat

* Upgrade d3 to latest to resolve d3-selection conflicts with nteract/data-explorer that broke D3ForceGraph

* Upgrade jupyterlab terminal widget to work with latest version of react. Upgrade jupyterlab services to include latest fix for websocket auth

* Update jest test snapshots

* Upgrade packages to fix build issues

* Remove comment

* Fix unit tests

* Fix unit test snapshot

* Remove useless @types/node-fetch
This commit is contained in:
Laurent Nguyen
2020-10-01 14:00:46 +02:00
committed by GitHub
parent 4fe2098730
commit 0ad5fb465b
21 changed files with 5135 additions and 11636 deletions

View File

@@ -1,15 +1,16 @@
/**
* JupyterLab applications based on jupyterLab components
*/
import { ServerConnection, TerminalSession } from "@jupyterlab/services";
import { ServerConnection, TerminalManager } from "@jupyterlab/services";
import { Terminal } from "@jupyterlab/terminal";
import { Panel, Widget } from "@phosphor/widgets";
export class JupyterLabAppFactory {
public static async createTerminalApp(serverSettings: ServerConnection.ISettings) {
const session = await TerminalSession.startNew({
const manager = new TerminalManager({
serverSettings: serverSettings
});
const session = await manager.startNew();
const term = new Terminal(session, { theme: "dark", shutdownOnClose: true });
if (!term) {
@@ -21,7 +22,7 @@ export class JupyterLabAppFactory {
term.addClass("terminalWidget");
let panel = new Panel();
panel.addWidget(term);
panel.addWidget(term as any);
panel.id = "main";
// Attach the widget to the dom.

View File

@@ -36,6 +36,7 @@ const createServerSettings = (urlVars: { [key: string]: string }): ServerConnect
options = {
baseUrl: server,
token: urlVars[TerminalQueryParams.Token],
appendToken: true,
init: { body },
fetch: window.parent.fetch
};