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
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	25	constructor(
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	26	private readonly _extension_uri: Uri,
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	27	private readonly _language_client: LanguageClient
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	28	) { }
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	request(language_client: LanguageClient) {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	31	if (language_client) {
83406 9b3a9d739c2e discontinue pointless "init" flag; wenzelm parents: 83388 diff changeset	32	this._language_client.sendNotification(lsp.documentation_request_type);
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	33	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	34	}
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	setupDocumentation(language_client: LanguageClient) {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	37	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	38	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	39	return;
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	40	}
83382 67c848a77c7e tuned: avoid camel-case; wenzelm parents: 83370 diff changeset	41	this._documentation_sections = params.sections;
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	42	if (this._view) {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	43	this._update_webview();
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	44	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	45	});
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
83370 6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	48	public resolveWebviewView(
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	49	view: WebviewView,
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	50	context: WebviewViewResolveContext,
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	51	_token: CancellationToken
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	52	): void {
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	53	this._view = view;
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	54	this._view.webview.options = {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	55	enableScripts: true,
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	56	localResourceRoots: [
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	57	this._extension_uri
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	58	]
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	59	};
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	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	62
83382 67c848a77c7e tuned: avoid camel-case; wenzelm parents: 83370 diff changeset	63	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	64	this._update_webview();
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	65	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	66
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	67	this._view.webview.onDidReceiveMessage(async message => {
83385 669b11a039bc clarified names; wenzelm parents: 83382 diff changeset	68	if (message.command === 'open_document') {
83388 8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path; wenzelm parents: 83385 diff changeset	69	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	70	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	71	});
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	private _update_webview(): void {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	75	if (!this._view) {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	76	return;
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
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	79	this._view.webview.postMessage({
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	80	command: 'update',
83382 67c848a77c7e tuned: avoid camel-case; wenzelm parents: 83370 diff changeset	81	sections: this._documentation_sections,
83363 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	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	84
83388 8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path; wenzelm parents: 83385 diff changeset	85	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	86	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	87
83388 8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path; wenzelm parents: 83385 diff changeset	88	if (platform_path.endsWith(".pdf")) {
8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path; wenzelm parents: 83385 diff changeset	89	commands.executeCommand("vscode.open", uri)
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	90	}
83388 8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path; wenzelm parents: 83385 diff changeset	91	else {
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	92	workspace.openTextDocument(uri).then(document => {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	93	window.showTextDocument(document);
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	94	});
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	95	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	96	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	97
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	private _get_html(): string {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	100	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	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
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	104	function get_webview_html(webview: Webview \| undefined, extension_path: string): string {
83370 6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	105	const script_uri =
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	106	webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'documentation.js')))
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	107	const css_uri =
6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	108	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	109	const font_uri =
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	110	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	111
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	112	return `
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	113	<!DOCTYPE html>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	114	<html lang="en">
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	115	<head>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	116	<meta charset="UTF-8">
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	117	<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	118	<link href="${css_uri}" rel="stylesheet">
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	119	<style>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	120	@font-face {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	121	font-family: "Isabelle DejaVu Sans Mono";
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	122	src: url(${font_uri});
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	123	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	124	${_get_decorations()}
83370 6a097e8add88 tuned whitespace; wenzelm parents: 83363 diff changeset	125	</style>
83363 486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	126	<title>Documentation Panel</title>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	127	</head>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	128	<body>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	129	<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	130	<script src="${script_uri}"></script>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	131	</body>
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	132	</html>`;
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	133	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	134
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	135	function _get_decorations(): string {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	136	let style: string[] = []
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	137	for (const key of text_colors) {
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	138	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	139	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	140	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	141	return style.join("")
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	142	}
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	143
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München; wenzelm parents: diff changeset	144	export { Documentation_Panel_Provider, get_webview_html };

author	wenzelm
	Mon, 03 Nov 2025 15:08:18 +0100
changeset 83478	65f9ca28cebf
parent 83406	9b3a9d739c2e
permissions	-rw-r--r--