--- 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
--- 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 `<!DOCTYPE html>
<html lang='en'>
--- 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)