# HG changeset patch # User Thomas Lindae # Date 1718218451 -7200 # Node ID 2d3a0728cf1cc3884992fcf1bae2f98df5a2e0be # Parent 45ef41e823f7065a800df44757cc90d30c310cc1 vscode: added all fonts to extension; diff -r 45ef41e823f7 -r 2d3a0728cf1c src/Tools/VSCode/extension/MANIFEST --- a/src/Tools/VSCode/extension/MANIFEST Wed Jun 12 20:44:10 2024 +0200 +++ b/src/Tools/VSCode/extension/MANIFEST Wed Jun 12 20:54:11 2024 +0200 @@ -11,7 +11,6 @@ media/ViewSource_inverse.svg media/ViewSource.svg media/vscode.css -media/IsabelleDejaVuSansMono.ttf package.json README.md src/abbreviations.ts diff -r 45ef41e823f7 -r 2d3a0728cf1c src/Tools/VSCode/extension/src/output_view.ts --- a/src/Tools/VSCode/extension/src/output_view.ts Wed Jun 12 20:44:10 2024 +0200 +++ b/src/Tools/VSCode/extension/src/output_view.ts Wed Jun 12 20:54:11 2024 +0200 @@ -85,7 +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'))) + const font_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'fonts', 'IsabelleDejaVuSansMono.ttf'))) return ` diff -r 45ef41e823f7 -r 2d3a0728cf1c src/Tools/VSCode/src/component_vscode_extension.scala --- a/src/Tools/VSCode/src/component_vscode_extension.scala Wed Jun 12 20:44:10 2024 +0200 +++ b/src/Tools/VSCode/src/component_vscode_extension.scala Wed Jun 12 20:54:11 2024 +0200 @@ -154,30 +154,32 @@ 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 = Isabelle_System.with_tmp_dir("build") { build_dir => val manifest_text = File.read(VSCode_Main.extension_dir + VSCode_Main.MANIFEST) val manifest_entries = split_lines(manifest_text).filter(_.nonEmpty) - val manifest_shasum: SHA1.Shasum = { - val a = SHA1.shasum_meta_info(SHA1.digest(manifest_text)) - val bs = - for (name <- manifest_entries) - yield SHA1.shasum(SHA1.digest(VSCode_Main.extension_dir + Path.explode(name)), name) - SHA1.flat_shasum(a :: bs) - } for (name <- manifest_entries) { val path = Path.explode(name) Isabelle_System.copy_file(VSCode_Main.extension_dir + path, Isabelle_System.make_directory(build_dir + path.dir)) } + + for (entry <- Isabelle_Fonts.fonts()) { + Isabelle_System.copy_file(entry.path, Isabelle_System.make_directory(build_dir + Path.basic("fonts"))) + } + val manifest_text2 = + manifest_text + cat_lines(Isabelle_Fonts.fonts().map(e => "fonts/" + e.path.file_name)) + val manifest_entries2 = split_lines(manifest_text2).filter(_.nonEmpty) + + val manifest_shasum: SHA1.Shasum = { + val a = SHA1.shasum_meta_info(SHA1.digest(manifest_text2)) + val bs = + for (name <- manifest_entries2) + yield SHA1.shasum(SHA1.digest(build_dir + Path.explode(name)), name) + SHA1.flat_shasum(a :: bs) + } File.write(build_dir + VSCode_Main.MANIFEST.shasum, manifest_shasum.toString) build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress)