Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: support placeholder queries that only request a subset of data #826

Merged
merged 9 commits into from
Jan 23, 2024
43 changes: 40 additions & 3 deletions packages/safe-ds-vscode/src/extension/messages.ts
Original file line number Diff line number Diff line change
Expand Up @@ -68,7 +68,27 @@ export interface ProgramMainInformation {
export interface PlaceholderQueryMessage {
type: 'placeholder_query';
id: string;
data: string;
data: PlaceholderQuery;
}

/**
* A query on a placeholder value.
*/
export interface PlaceholderQuery {
/**
* The name of the requested placeholder.
*/
name: string;

/**
* The offset of the requested data.
*/
window_begin?: number;

/**
* The size of the requested data.
*/
window_size?: number;
WinPlay02 marked this conversation as resolved.
Show resolved Hide resolved
}

// Python Server to Extension
Expand Down Expand Up @@ -105,6 +125,10 @@ export interface PlaceholderValue {
name: string;
type: string;
value: string;
windowed?: boolean;
window_begin?: number;
window_size?: number;
window_max?: number;
WinPlay02 marked this conversation as resolved.
Show resolved Hide resolved
}

// Python Server to Extension
Expand Down Expand Up @@ -152,8 +176,21 @@ export const createProgramMessage = function (id: string, data: ProgramPackageMa
return { type: 'program', id, data };
};

export const createPlaceholderQueryMessage = function (id: string, placeholderName: string): PythonServerMessage {
return { type: 'placeholder_query', id, data: placeholderName };
export const createPlaceholderQueryMessage = function (
id: string,
placeholderName: string,
windowBegin: number | undefined = undefined,
windowSize: number | undefined = undefined,
): PythonServerMessage {
return {
type: 'placeholder_query',
id,
data: {
name: placeholderName,
window_begin: !windowBegin ? undefined : Math.round(windowBegin),
window_size: !windowSize ? undefined : Math.round(windowSize),
},
};
};

// Extension to Python Server
Expand Down
Loading