--- a/src/Tools/VSCode/extension/MANIFEST Mon May 27 13:18:29 2024 +0200
+++ b/src/Tools/VSCode/extension/MANIFEST Mon May 27 13:20:31 2024 +0200
@@ -11,6 +11,7 @@
media/ViewSource_inverse.svg
media/ViewSource.svg
media/vscode.css
+media/IsabelleDejaVuSansMono.ttf
package.json
README.md
src/abbreviations.ts
--- a/src/Tools/VSCode/extension/media/vscode.css Mon May 27 13:18:29 2024 +0200
+++ b/src/Tools/VSCode/extension/media/vscode.css Mon May 27 13:20:31 2024 +0200
@@ -9,12 +9,16 @@
body {
padding: 0 var(--container-paddding);
color: var(--vscode-foreground);
- font-size: var(--vscode-font-size);
- font-weight: var(--vscode-font-weight);
- font-family: var(--vscode-font-family);
+ font-size: var(--vscode-editor-font-size);
+ font-weight: var(--vscode-editor-font-weight);
+ font-family: var(--vscode-editor-font-family);
background-color: var(--vscode-editor-background);
}
+pre {
+ font-family: var(--vscode-editor-font-family);
+}
+
ol,
ul {
padding-left: var(--container-paddding);
@@ -79,7 +83,7 @@
display: block;
width: 100%;
border: none;
- font-family: var(--vscode-font-family);
+ font-family: var(--vscode-editor-font-family);
padding: var(--input-padding-vertical) var(--input-padding-horizontal);
color: var(--vscode-input-foreground);
outline-color: var(--vscode-input-border);
@@ -110,4 +114,4 @@
white-space: -pre-wrap; /* Opera 4-6 */
white-space: -o-pre-wrap; /* Opera 7 */
word-wrap: break-word; /* Internet Explorer 5.5+ */
-}
\ No newline at end of file
+}
--- a/src/Tools/VSCode/extension/src/output_view.ts Mon May 27 13:18:29 2024 +0200
+++ b/src/Tools/VSCode/extension/src/output_view.ts Mon May 27 13:20:31 2024 +0200
@@ -85,6 +85,7 @@
{
const script_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'main.js')))
const css_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'vscode.css')))
+ const font_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'IsabelleDejaVuSansMono.ttf')))
return `<!DOCTYPE html>
<html lang='en'>
@@ -93,7 +94,11 @@
<meta name='viewport' content='width=device-width, initial-scale=1.0'>
<link href='${css_uri}' rel='stylesheet' type='text/css'>
<style>
- ${_get_decorations()}
+ @font-face {
+ font-family: "Isabelle DejaVu Sans Mono";
+ src: url(${font_uri});
+ }
+ ${_get_decorations()}
</style>
<title>Output</title>
</head>
--- a/src/Tools/VSCode/src/component_vscode_extension.scala Mon May 27 13:18:29 2024 +0200
+++ b/src/Tools/VSCode/src/component_vscode_extension.scala Mon May 27 13:20:31 2024 +0200
@@ -154,6 +154,12 @@
Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
+ /* font for output/state panel */
+
+ val font_path = Isabelle_Fonts.fonts().find(e => e.name == Isabelle_Fonts.mono).get.path
+ Isabelle_System.copy_file(font_path, VSCode_Main.extension_dir + Path.basic("media"))
+
+
/* build */
val vsix_name =