UI: LogBox overhaul (#508)

This commit is contained in:
David Walker
2023-05-26 05:07:37 -07:00
committed by GitHub
parent 113af6e711
commit 4503da6226
26 changed files with 431 additions and 114 deletions

View File

@@ -169,6 +169,29 @@ interface Multipliers {
bladeburner_success_chance: number;
}
/** @public */
interface TailProperties {
/** X-coordinate of the log window */
x: number;
/** Y-coordinate of the log window */
y: number;
/** Width of the log window content area */
width: number;
/** Height of the log window content area */
height: number;
}
/**
* @public
* A stand-in for the real React.ReactElement, which API-extractor doesn't know about.
* Don't try to create one of these by hand; use React.createElement().
*/
interface ReactElement {
type: string | ((props: any) => ReactElement | null) | (new (props: any) => object);
props: any;
key: string | number | null;
}
/** @public */
interface RunningScript {
/** Arguments the script was called with */
@@ -198,6 +221,15 @@ interface RunningScript {
ramUsage: number;
/** Hostname of the server on which this script runs */
server: string;
/** Properties of the tail window, or null if it is not shown */
tailProperties: TailProperties | null;
/**
* The title, as shown in the script's log box. Defaults to the name + args,
* but can be changed by the user. If it is set to a React element (only by
* the user), that will not be persisted, and will be restored to default on
* load.
*/
title: string | ReactElement;
/** Number of threads that this script runs with */
threads: number;
/** Whether this RunningScript is excluded from saves */
@@ -5103,6 +5135,29 @@ export interface NS {
*/
closeTail(pid?: number): void;
/**
* Set the title of the tail window of a script.
* @remarks
* RAM cost: 0 GB
*
* This sets the title to the given string, and also forces an update of the
* tail window's contents.
*
* The title is saved across restarts, but only if it is a simple string.
*
* If the pid is unspecified, it will modify the current scripts logs.
*
* Otherwise, the pid argument can be used to change the logs from another script.
*
* It is possible to pass a React Element instead of a string. Get these by calling
* React.createElement() with appropriate parameters. You should either know
* or be willing to learn about the React UI library if you go down this
* route, and there will likely be rough edges.
*
* @param pid - Optional. PID of the script having its tail closed. If omitted, the current script is used.
*/
setTitle(title: string | ReactElement, pid?: number): void;
/**
* Get the list of servers connected to a server.
* @remarks