/* Author: Diana Korchmar, LMU Muenchen
Author : Makarius
Isabelle symbols panel as web view .
*/
"use strict" ;
import {
WebviewViewProvider, WebviewView, Uri, WebviewViewResolveContext,
CancellationToken, window, Position, Selection, Webview
} from "vscode"
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" ;
import * as symbol from './symbol'
class Symbols_Panel_Provider implements WebviewViewProvider {
public static readonly view_type = "isabelle-symbols"
private _view?: WebviewView
private _grouped_symbols: { [key: string]: symbol.Entry[] } = {}
private _abbrevs: [string, string][] = [];
constructor(
private readonly _extension_uri: Uri,
private readonly _language_client: LanguageClient
) { }
request( language_client: LanguageClient) {
if (language_client) {
this ._language_client.sendNotification(lsp.abbrevs_request_type);
}
}
setup(language_client: LanguageClient) {
language_client.onNotification(lsp.abbrevs_response_type, params => {
this ._grouped_symbols = this ._group_symbols(symbol.symbols.entries);
this ._abbrevs = params.abbrevs ?? [];
if (this ._view) {
this ._update_webview();
}
});
}
public resolveWebviewView(
view: WebviewView,
context: WebviewViewResolveContext,
_token: CancellationToken) {
this ._view = view
view.webview.options = {
enableScripts: true ,
localResourceRoots: [
this ._extension_uri
]
}
view.webview.html = this ._get_html()
if (Object.keys(this ._grouped_symbols).length > 0 ) {
this ._update_webview();
}
this ._view.webview.onDidReceiveMessage(message => {
if (message.command === "insert_symbol" ) {
this ._insert_symbol(message.symbol);
}
else if (message.command === "reset_control" ) {
this ._reset_control();
}
else if (message.command === "apply_control" ) {
this ._apply_control(message.action);
}
});
}
private _apply_control(action: string): void {
const editor = window.activeTextEditor;
if (!editor) return ;
const document = editor.document;
const selection = editor.selection;
let selected_text = document.getText(selection);
if (!selected_text.trim() && !selection.isEmpty) return ;
const control_symbols: { [key: string]: string } = {};
symbol.control_render.forEach(symbol => control_symbols[symbol.name] = symbol.decoded);
if (!control_symbols[action]) return ;
const control_symbol = control_symbols[action];
const all_control_symbols = Object.values(control_symbols);
editor.edit(edit_builder => {
if (!selection.isEmpty) {
let new_text = selected_text
.split("" )
.map((char , index, arr) => {
if (char .trim() === "" ) return char ;
if (all_control_symbols.includes(char )) return "" ;
return `${control_symbol}${char }`;
})
.join("" );
edit_builder.replace(selection, new_text);
}
else {
edit_builder.insert(selection.active, control_symbol);
}
}).then(success => {
if (!success) {
window.showErrorMessage("Failed to apply control effect." );
}
});
}
private _insert_symbol(symbol: string): void {
const editor = window.activeTextEditor;
if (editor) {
editor.edit(edit_builder => edit_builder.insert(editor.selection.active, symbol));
}
}
private _reset_control(): void {
const editor = window.activeTextEditor;
if (!editor) {
return ;
}
const document = editor.document;
const selection = editor.selection;
let selected_text = document.getText(selection);
if (!selected_text.trim() && !selection.isEmpty) return ;
const control_symbols: { [key: string]: string } = {};
symbol.control_render.forEach(symbol => control_symbols[symbol.decoded] = symbol.name);
const all_control_symbols = Object.keys(control_symbols);
editor.edit(edit_builder => {
if (!selection.isEmpty) {
let new_text = selected_text
.split("" )
.map(char => (all_control_symbols.includes(char ) ? "" : char ))
.join("" );
edit_builder.replace(selection, new_text);
}
}).then(success => {
if (!success) {
}
});
}
private _update_webview(): void {
this ._view.webview.postMessage({
command: "update" ,
symbols: this ._grouped_symbols,
abbrevs: this ._abbrevs,
});
}
private _group_symbols(symbols: symbol.Entry[]): { [key: string]: symbol.Entry[] } {
const grouped_symbols: { [key: string]: symbol.Entry[] } = {};
for (const symbol of symbols) {
if (symbol.groups && Array.isArray(symbol.groups)) {
for (const group of symbol.groups) {
if (!grouped_symbols[group]) {
grouped_symbols[group] = [];
}
grouped_symbols[group].push(symbol);
}
}
}
return grouped_symbols;
}
private _get_html(): string {
return get_webview_html(this ._view.webview, this ._extension_uri.fsPath)
}
}
function open_webview_link(link: string) {
const uri = Uri.parse(link)
const line = Number(uri.fragment) || 0
const pos = new Position(line, 0 )
window.showTextDocument(uri.with({ fragment: "" }), {
preserveFocus: false ,
selection: new Selection(pos, pos)
})
}
function get_webview_html(webview: Webview, extension_path: string): string {
const script_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, "media" , "symbols.js" )))
const css_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, "media" , "symbols.css" )))
const font_uri =
webview.asWebviewUri(Uri.file(path.join(extension_path, "fonts" , "IsabelleDejaVuSansMono.ttf" )))
return `<!DOCTYPE html>
<html lang="en" >
<head>
<meta charset="UTF-8" >
<meta name="viewport" content="width=device-width, initial-scale=1.0" >
<link href="${css_uri}" rel="stylesheet" type="text/css" >
<style>
@font-face {
font-family: "Isabelle DejaVu Sans Mono" ;
src: url(${font_uri});
}
${_get_decorations()}
</style>
<title>Symbols Panel</title>
</head>
<body>
<div id="symbols-container" ></div>
<script src="${script_uri}" ></script>
</body>
</html>`
}
function _get_decorations(): string {
let style: string[] = []
for (const key of text_colors) {
style.push(`body.vscode-light .${key} { color: ${vscode_lib.get_color(key, true )} }\n`)
style.push(`body.vscode-dark .${key} { color: ${vscode_lib.get_color(key, false )} }\n`)
}
return style.join("" )
}
export { Symbols_Panel_Provider, get_webview_html, open_webview_link }
Messung V0.5 in Prozent C=97 H=96 G=96
¤ Dauer der Verarbeitung: 0.35 Sekunden
(vorverarbeitet am 2026-07-03)
¤
*© Formatika GbR, Deutschland