message: Implement showNumberInput() for the extension API
diff: @@ -15,6 +15,7 @@ import {EtTerminal} from './Terminal';
  import {ViewerElement} from './ViewerElement';
  import {TextViewer} from'./viewers/TextViewer';
  import OwnerTrackingList from './utils/OwnerTrackingList';
  +import {PopDownNumberDialog} from './gui/PopDownNumberDialog';
  interface ActiveExtension {
  @@ -190,6 +191,8 @@ class WorkspaceProxy implements ExtensionApi.Workspace {
  class TerminalProxy implements ExtensionApi.Terminal {
  + private _numberInputDialog: PopDownNumberDialog = null;
  +
  constructor(private _extensionContextImpl: ExtensionContextImpl, private _terminal: EtTerminal) {
  }
  @@ -197,8 +200,30 @@ class TerminalProxy implements ExtensionApi.Terminal {
  this._terminal.send(text);
  }
  +// FIXME move this the bridge
  showNumberInput(options: ExtensionApi.NumberInputOptions): Promise<number | undefined> {
  -return null;
  + if (this._numberInputDialog == null) {
  + this._numberInputDialog = <PopDownNumberDialog> window.document.createElement(PopDownNumberDialog.TAG_NAME);
  + window.document.body.appendChild(this._numberInputDialog);
  + }
  + this._numberInputDialog.setTitlePrimary(options.title);
  + this._numberInputDialog.setMinimum(options.minimum !== undefined ? options.minimum : Number.MIN_SAFE_INTEGER);
  + this._numberInputDialog.setMaximum(options.maximum !== undefined ? options.maximum : Number.MAX_SAFE_INTEGER);
  + this._numberInputDialog.setValue(options.value);
  +
  + const rect = this._terminal.getBoundingClientRect();
  + this._numberInputDialog.open(rect.left, rect.top, rect.width, rect.height);
  + this._numberInputDialog.focus();
  +
  + return new Promise((resolve, reject) => {
  + const selectedHandler = (ev: CustomEvent): void => {
  + this._numberInputDialog.removeEventListener('selected', selectedHandler);
  + resolve(ev.detail.value == null ? undefined : ev.detail.value);
  + this._terminal.focus();
  + };
  +
  + this._numberInputDialog.addEventListener('selected', selectedHandler);
  + });
  }
  }
  