isabelle: src/Tools/VSCode/extension/src/documentation

83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	1	/* Author: Diana Korchmar, LMU Muenchen
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	2
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	3	Isabelle documentation panel as web view.
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	4	*/
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	5
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	6	'use strict';
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	7
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	8	import {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	9	WebviewViewProvider, WebviewView, Uri, WebviewViewResolveContext,
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	10	CancellationToken, window, workspace, Webview, env
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	11	} from 'vscode'
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	12	import { text_colors } from './decorations'
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	13	import * as vscode_lib from './vscode_lib'
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	14	import * as path from 'path'
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	15	import * as lsp from './lsp'
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	16	import { commands } from 'vscode'
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	17	import { LanguageClient } from 'vscode-languageclient/node';
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	18
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	19	class Documentation_Panel_Provider implements WebviewViewProvider {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	20	public static readonly view_type = 'isabelle-documentation';
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	21
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	22	private _view?: WebviewView;
83382 67c848a77c7e tuned: avoid camel-case; wenzelm parents: 83370 diff changeset	23	private _documentation_sections: any[] = [];
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	24	private _initialized = false;
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	25
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	26	constructor(
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	27	private readonly _extension_uri: Uri,
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	28	private readonly _language_client: LanguageClient
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	29	) { }
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	30
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	31	request(language_client: LanguageClient) {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	32	if (language_client) {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	33	this._language_client.sendNotification(lsp.documentation_request_type, { init: true });
83370 6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	34
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	35	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	36	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	37
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	38	setupDocumentation(language_client: LanguageClient) {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	39	language_client.onNotification(lsp.documentation_response_type, params => {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	40	if (!params \|\| !params.sections \|\| !Array.isArray(params.sections)) {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	41	return;
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	42	}
83382 67c848a77c7e tuned: avoid camel-case; wenzelm parents: 83370 diff changeset	43	this._documentation_sections = params.sections;
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	44	if (this._view) {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	45	this._update_webview();
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	46	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	47	});
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	48	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	49
83370 6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	50	public resolveWebviewView(
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	51	view: WebviewView,
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	52	context: WebviewViewResolveContext,
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	53	_token: CancellationToken
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	54	): void {
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	55	this._view = view;
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	56	this._view.webview.options = {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	57	enableScripts: true,
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	58	localResourceRoots: [
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	59	this._extension_uri
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	60	]
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	61	};
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	62
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	63	this._view.webview.html = this._get_html();
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	64
83382 67c848a77c7e tuned: avoid camel-case; wenzelm parents: 83370 diff changeset	65	if (Object.keys(this._documentation_sections).length > 0) {
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	66	this._update_webview();
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	67	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	68
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	69	this._view.webview.onDidReceiveMessage(async message => {
83385 669b11a039bc clarified names; wenzelm parents: 83382 diff changeset	70	if (message.command === 'open_document') {
83388 8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path; wenzelm parents: 83385 diff changeset	71	this._open_document(message.platform_path);
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	72	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	73	});
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	74
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	75	this._initialized = true;
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	76	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	77
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	78	private _update_webview(): void {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	79	if (!this._view) {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	80	return;
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	81	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	82
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	83	this._view.webview.postMessage({
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	84	command: 'update',
83382 67c848a77c7e tuned: avoid camel-case; wenzelm parents: 83370 diff changeset	85	sections: this._documentation_sections,
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	86	});
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	87	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	88
83388 8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path; wenzelm parents: 83385 diff changeset	89	private _open_document(platform_path: string): void {
8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path; wenzelm parents: 83385 diff changeset	90	const uri = Uri.file(platform_path);
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	91
83388 8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path; wenzelm parents: 83385 diff changeset	92	if (platform_path.endsWith(".pdf")) {
8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path; wenzelm parents: 83385 diff changeset	93	commands.executeCommand("vscode.open", uri)
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	94	}
83388 8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path; wenzelm parents: 83385 diff changeset	95	else {
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	96	workspace.openTextDocument(uri).then(document => {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	97	window.showTextDocument(document);
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	98	});
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	99	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	100	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	101
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	102
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	103	private _get_html(): string {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	104	return get_webview_html(this._view?.webview, this._extension_uri.fsPath);
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	105	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	106	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	107
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	108	function get_webview_html(webview: Webview \| undefined, extension_path: string): string {
83370 6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	109	const script_uri =
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	110	webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'documentation.js')))
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	111	const css_uri =
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	112	webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'documentation.css')))
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	113	const font_uri =
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	114	webview.asWebviewUri(Uri.file(path.join(extension_path, 'fonts', 'IsabelleDejaVuSansMono.ttf')))
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	115
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	116	return `
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	117	<!DOCTYPE html>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	118	<html lang="en">
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	119	<head>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	120	<meta charset="UTF-8">
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	121	<meta name="viewport" content="width=device-width, initial-scale=1.0">
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	122	<link href="${css_uri}" rel="stylesheet">
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	123	<style>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	124	@font-face {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	125	font-family: "Isabelle DejaVu Sans Mono";
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	126	src: url(${font_uri});
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	127	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	128	${_get_decorations()}
83370 6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	129	</style>
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	130	<title>Documentation Panel</title>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	131	</head>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	132	<body>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	133	<div id="documentation-container">Loading documentation...</div>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	134	<script src="${script_uri}"></script>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	135	</body>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	136	</html>`;
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	137	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	138
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	139	function _get_decorations(): string {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	140	let style: string[] = []
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	141	for (const key of text_colors) {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	142	style.push(`body.vscode-light .${key} { color: ${vscode_lib.get_color(key, true)} }\n`)
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	143	style.push(`body.vscode-dark .${key} { color: ${vscode_lib.get_color(key, false)} }\n`)
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	144	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	145	return style.join("")
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	146	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	147
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	148	export { Documentation_Panel_Provider, get_webview_html };

author	wenzelm
	Sat, 25 Oct 2025 19:54:47 +0200
changeset 83388	8d90bd0e4f39
parent 83385	669b11a039bc
child 83406	9b3a9d739c2e
permissions	-rw-r--r--