# HG changeset patch # User Thomas Lindae # Date 1716808831 -7200 # Node ID 07d25a1830df1c70f1d20a0a32eed7dd0983dbbb # Parent 6206f3b2625ab2814d5e87f760fec3bdfd7f5ce6 vscode: IsabelleDejaVuSansMono for state and output panel; diff -r 6206f3b2625a -r 07d25a1830df src/Tools/VSCode/extension/MANIFEST --- 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 diff -r 6206f3b2625a -r 07d25a1830df src/Tools/VSCode/extension/media/vscode.css --- 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 +} diff -r 6206f3b2625a -r 07d25a1830df src/Tools/VSCode/extension/src/output_view.ts --- 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 ` @@ -93,7 +94,11 @@ Output diff -r 6206f3b2625a -r 07d25a1830df src/Tools/VSCode/src/component_vscode_extension.scala --- 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 =