Docked auto py-terminal (#1284)

This commit is contained in:
Andrea Giammarchi
2023-03-20 11:22:16 +01:00
committed by GitHub
parent 716254e655
commit e10d055453
5 changed files with 99 additions and 23 deletions

View File

@@ -6,8 +6,25 @@ import { getLogger } from '../logger';
import { type Stdio } from '../stdio';
import { InterpreterClient } from '../interpreter_client';
type AppConfigStyle = AppConfig & { terminal?: boolean | 'auto'; docked?: boolean | 'docked' };
const logger = getLogger('py-terminal');
const validate = (config: AppConfigStyle, name: string, default_: string) => {
const value = config[name] as undefined | boolean | string;
if (value !== undefined && value !== true && value !== false && value !== default_) {
const got = JSON.stringify(value);
throw new UserError(
ErrorCode.BAD_CONFIG,
`Invalid value for config.${name}: the only accepted` +
`values are true, false and "${default_}", got "${got}".`,
);
}
if (value === undefined) {
config[name] = default_;
}
};
export class PyTerminalPlugin extends Plugin {
app: PyScriptApp;
@@ -16,33 +33,24 @@ export class PyTerminalPlugin extends Plugin {
this.app = app;
}
configure(config: AppConfig & { terminal?: boolean | 'auto' }) {
configure(config: AppConfigStyle) {
// validate the terminal config and handle default values
const t = config.terminal;
if (t !== undefined && t !== true && t !== false && t !== 'auto') {
const got = JSON.stringify(t);
throw new UserError(
ErrorCode.BAD_CONFIG,
'Invalid value for config.terminal: the only accepted' +
`values are true, false and "auto", got "${got}".`,
);
}
if (t === undefined) {
config.terminal = 'auto'; // default value
}
validate(config, 'terminal', 'auto');
validate(config, 'docked', 'docked');
}
beforeLaunch(config: AppConfig & { terminal?: boolean | 'auto' }) {
beforeLaunch(config: AppConfigStyle) {
// if config.terminal is "yes" or "auto", let's add a <py-terminal> to
// the document, unless it's already present.
const t = config.terminal;
if (t === true || t === 'auto') {
if (document.querySelector('py-terminal') === null) {
logger.info('No <py-terminal> found, adding one');
const termElem = document.createElement('py-terminal');
if (t === 'auto') termElem.setAttribute('auto', '');
document.body.appendChild(termElem);
}
const { terminal: t, docked: d } = config;
const auto = t === true || t === 'auto';
const docked = d === true || d === 'docked';
if (auto && document.querySelector('py-terminal') === null) {
logger.info('No <py-terminal> found, adding one');
const termElem = document.createElement('py-terminal');
if (auto) termElem.setAttribute('auto', '');
if (docked) termElem.setAttribute('docked', '');
document.body.appendChild(termElem);
}
}
@@ -93,6 +101,10 @@ function make_PyTerminal(app: PyScriptApp) {
this.autoShowOnNextLine = false;
}
if (this.isDocked()) {
this.classList.add('py-terminal-docked');
}
logger.info('Registering stdio listener');
app.registerStdioListener(this);
}
@@ -101,9 +113,16 @@ function make_PyTerminal(app: PyScriptApp) {
return this.hasAttribute('auto');
}
isDocked() {
return this.hasAttribute('docked');
}
// implementation of the Stdio interface
stdout_writeline(msg: string) {
this.outElem.innerText += msg + '\n';
if (this.isDocked()) {
this.scrollTop = this.scrollHeight;
}
if (this.autoShowOnNextLine) {
this.classList.remove('py-terminal-hidden');
this.autoShowOnNextLine = false;