# HG changeset patch
# User wenzelm
# Date 1648157747 -3600
# Node ID aeda3606c405c46d9a0b25b70887a227d234f571
# Parent  8f0d94fb8551c37298ce9202ab273e81afaea99b
tuned;

diff -r 8f0d94fb8551 -r aeda3606c405 src/Tools/VSCode/src/vscode_main.scala
--- a/src/Tools/VSCode/src/vscode_main.scala	Thu Mar 24 22:27:17 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_main.scala	Thu Mar 24 22:35:47 2022 +0100
@@ -78,35 +78,11 @@
   def default_vsix_path: Path = Path.explode("$ISABELLE_VSCODE_VSIX")
 
   def extension_dir: Path = Path.explode("$ISABELLE_VSCODE_HOME/extension")
+  val extension_name: String = "isabelle.isabelle"
   def extension_manifest(): Manifest = new Manifest
-  val extension_name: String = "isabelle.isabelle"
 
   private val MANIFEST: Path = Path.explode("MANIFEST")
 
-  private def shasum_vsix(vsix_path: Path): String =
-  {
-    val name = "extension/MANIFEST.shasum"
-    def err(): Nothing = error("Cannot retrieve " + quote(name) + " from " + vsix_path)
-    if (vsix_path.is_file) {
-      using(new ZipFile(vsix_path.file))(zip_file =>
-      {
-        val entry = zip_file.getEntry(name)
-        if (entry == null) err()
-        else {
-          val stream = zip_file.getInputStream(entry)
-          if (stream == null) err() else File.read_stream(stream)
-        }
-      })
-    }
-    else err()
-  }
-
-  private def shasum_dir(dir: Path): Option[String] =
-  {
-    val path = dir + MANIFEST.shasum
-    if (path.is_file) Some(File.read(path)) else None
-  }
-
   final class Manifest private[VSCode_Main]
   {
     private val text = File.read(extension_dir + MANIFEST)
@@ -132,6 +108,30 @@
     }
   }
 
+  private def shasum_vsix(vsix_path: Path): String =
+  {
+    val name = "extension/MANIFEST.shasum"
+    def err(): Nothing = error("Cannot retrieve " + quote(name) + " from " + vsix_path)
+    if (vsix_path.is_file) {
+      using(new ZipFile(vsix_path.file))(zip_file =>
+        zip_file.getEntry(name) match {
+          case null => err()
+          case entry =>
+            zip_file.getInputStream(entry) match {
+              case null => err()
+              case stream => File.read_stream(stream)
+            }
+        })
+    }
+    else err()
+  }
+
+  private def shasum_dir(dir: Path): Option[String] =
+  {
+    val path = dir + MANIFEST.shasum
+    if (path.is_file) Some(File.read(path)) else None
+  }
+
   def locate_extension(): Option[Path] =
   {
     val out = run_vscodium(List("--locate-extension", extension_name)).check.out