--- 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;
+}());
--- 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))
--- 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<Dynamic_Output>("PIDE/dynamic_output")
+export interface Output_Set_Margin
+{
+ margin: number
+}
+
+export const output_set_margin_type =
+ new NotificationType<Output_Set_Margin>("PIDE/output_set_margin")
/* state */
@@ -69,6 +76,15 @@
export const state_output_type =
new NotificationType<State_Output>("PIDE/state_output")
+export interface State_Set_Margin
+{
+ id: number
+ margin: number
+}
+
+export const state_set_margin_type =
+ new NotificationType<State_Set_Margin>("PIDE/state_set_margin")
+
export interface State_Id
{
id: number
@@ -80,7 +96,7 @@
enabled: boolean
}
-export const state_init_type = new NotificationType<void>("PIDE/state_init")
+export const state_init_type = new RequestType0("PIDE/state_init")
export const state_exit_type = new NotificationType<State_Id>("PIDE/state_exit")
export const state_locate_type = new NotificationType<State_Id>("PIDE/state_locate")
export const state_update_type = new NotificationType<State_Id>("PIDE/state_update")
--- 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
}
})
}
--- 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)
}
}