# HG changeset patch # User Thomas Lindae # Date 1717029901 -7200 # Node ID 56594fac1dabe8283d013be91c6526871d72b75d # Parent 50082e028475944da4d18c0b9d938cabade1d98a vscode: added dynamic and state output set margin messages to vscode extension; diff -r 50082e028475 -r 56594fac1dab src/Tools/VSCode/extension/media/main.js --- a/src/Tools/VSCode/extension/media/main.js Sun Jun 30 15:29:44 2024 +0200 +++ b/src/Tools/VSCode/extension/media/main.js Thu May 30 02:45:01 2024 +0200 @@ -1,6 +1,6 @@ (function () { const vscode = acquireVsCodeApi(); - + for (const link of document.querySelectorAll('a[href^="file:"]')) { link.addEventListener('click', () => { vscode.postMessage({ @@ -9,19 +9,43 @@ }); }); } - + const auto_update = document.getElementById('auto_update'); - auto_update && auto_update.addEventListener('change', (e) => { + auto_update && auto_update.addEventListener('change', e => { vscode.postMessage({'command': 'auto_update', 'enabled': e.target.checked}) ; }); const update_button = document.getElementById('update_button'); - update_button && update_button.addEventListener('click', (e) => { - vscode.postMessage({'command': 'update'}) + update_button && update_button.addEventListener('click', e => { + vscode.postMessage({'command': 'update'}) }); - + const locate_button = document.getElementById('locate_button'); - locate_button && locate_button.addEventListener('click', (e) => { + locate_button && locate_button.addEventListener('click', e => { vscode.postMessage({'command': 'locate'}); }); -}()); \ No newline at end of file + + const get_window_margin = () => { + const test_string = "a"; + const test_span = document.createElement("span"); + test_span.textContent = test_string; + document.body.appendChild(test_span); + const symbol_width = test_span.getBoundingClientRect().width / test_string.length; + document.body.removeChild(test_span); + + const width = window.innerWidth / symbol_width; + const result = Math.max(width - 16, 1); // extra headroom + return result; + } + + const update_window_width = () => { + vscode.postMessage({'command': 'resize', 'margin': get_window_margin()}) + }; + + var timeout; + window.onresize = function() { + clearTimeout(timeout); + timeout = setTimeout(update_window_width, 500); + }; + window.onload = update_window_width; +}()); diff -r 50082e028475 -r 56594fac1dab src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Sun Jun 30 15:29:44 2024 +0200 +++ b/src/Tools/VSCode/extension/src/extension.ts Thu May 30 02:45:01 2024 +0200 @@ -191,7 +191,7 @@ /* dynamic output */ - const provider = new Output_View_Provider(context.extensionUri) + const provider = new Output_View_Provider(context.extensionUri, language_client) context.subscriptions.push( window.registerWebviewViewProvider(Output_View_Provider.view_type, provider)) diff -r 50082e028475 -r 56594fac1dab src/Tools/VSCode/extension/src/lsp.ts --- a/src/Tools/VSCode/extension/src/lsp.ts Sun Jun 30 15:29:44 2024 +0200 +++ b/src/Tools/VSCode/extension/src/lsp.ts Thu May 30 02:45:01 2024 +0200 @@ -7,7 +7,7 @@ 'use strict'; import { MarkdownString } from 'vscode' -import { NotificationType } from 'vscode-languageclient' +import { NotificationType, RequestType0 } from 'vscode-languageclient' /* decorations */ @@ -56,6 +56,13 @@ export const dynamic_output_type = new NotificationType("PIDE/dynamic_output") +export interface Output_Set_Margin +{ + margin: number +} + +export const output_set_margin_type = + new NotificationType("PIDE/output_set_margin") /* state */ @@ -69,6 +76,15 @@ export const state_output_type = new NotificationType("PIDE/state_output") +export interface State_Set_Margin +{ + id: number + margin: number +} + +export const state_set_margin_type = + new NotificationType("PIDE/state_set_margin") + export interface State_Id { id: number @@ -80,7 +96,7 @@ enabled: boolean } -export const state_init_type = new NotificationType("PIDE/state_init") +export const state_init_type = new RequestType0("PIDE/state_init") export const state_exit_type = new NotificationType("PIDE/state_exit") export const state_locate_type = new NotificationType("PIDE/state_locate") export const state_update_type = new NotificationType("PIDE/state_update") diff -r 50082e028475 -r 56594fac1dab src/Tools/VSCode/extension/src/output_view.ts --- a/src/Tools/VSCode/extension/src/output_view.ts Sun Jun 30 15:29:44 2024 +0200 +++ b/src/Tools/VSCode/extension/src/output_view.ts Thu May 30 02:45:01 2024 +0200 @@ -10,6 +10,8 @@ import { text_colors } from './decorations' import * as vscode_lib from './vscode_lib' import * as path from 'path' +import * as lsp from './lsp' +import { LanguageClient } from 'vscode-languageclient/node'; class Output_View_Provider implements WebviewViewProvider @@ -20,7 +22,7 @@ private _view?: WebviewView private content: string = '' - constructor(private readonly _extension_uri: Uri) { } + constructor(private readonly _extension_uri: Uri, private readonly _language_client: LanguageClient) { } public resolveWebviewView( view: WebviewView, @@ -40,9 +42,14 @@ view.webview.html = this._get_html(this.content) view.webview.onDidReceiveMessage(async message => - { - if (message.command === 'open') { - open_webview_link(message.link) + { + switch (message.command) { + case "open": + open_webview_link(message.link) + break + case "resize": + this._language_client.sendNotification(lsp.output_set_margin_type, { margin: message.margin }) + break } }) } diff -r 50082e028475 -r 56594fac1dab src/Tools/VSCode/extension/src/state_panel.ts --- a/src/Tools/VSCode/extension/src/state_panel.ts Sun Jun 30 15:29:44 2024 +0200 +++ b/src/Tools/VSCode/extension/src/state_panel.ts Thu May 30 02:45:01 2024 +0200 @@ -61,6 +61,9 @@ case "open": open_webview_link(message.link) break + case "resize": + language_client.sendNotification(lsp.state_set_margin_type, { id: this.state_id, margin: message.margin }) + break default: break } @@ -97,7 +100,7 @@ { if (language_client) { if (panel) panel.reveal() - else language_client.sendNotification(lsp.state_init_type) + else language_client.sendRequest(lsp.state_init_type, null) } }