# HG changeset patch
# User wenzelm
# Date 1625857558 -7200
# Node ID 110a027a5473a11e1107b60859f7577b952f6123
# Parent  ac1884965dc80cf9edc02b94e63bb4695291ae71
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;

diff -r ac1884965dc8 -r 110a027a5473 src/Tools/Setup/isabelle/setup/Build.java
--- a/src/Tools/Setup/isabelle/setup/Build.java	Fri Jul 09 21:03:58 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build.java	Fri Jul 09 21:05:58 2021 +0200
@@ -98,11 +98,23 @@
         public List<String> resources() { return get_list("resources"); }
         public List<String> services() { return get_list("services"); }
 
-        public Path path(String file) { return _dir.resolve(file); }
-        public boolean exists(String file) { return Files.exists(path(file)); }
+        public Path path(String file)
+            throws IOException, InterruptedException
+        {
+            return _dir.resolve(Environment.expand_platform_path(file));
+        }
+        public boolean exists(String file)
+            throws IOException, InterruptedException
+        {
+            return Files.exists(path(file));
+        }
 
         // historic
-        public Path shasum_path() { return path(lib_name() + ".shasum"); }
+        public Path shasum_path()
+            throws IOException, InterruptedException
+        {
+            return path(lib_name() + ".shasum");
+        }
 
         public String item_name(String s)
         {
@@ -135,7 +147,7 @@
         }
 
         public String shasum(String file)
-            throws IOException, NoSuchAlgorithmException
+            throws IOException, NoSuchAlgorithmException, InterruptedException
         {
             return shasum(file, List.of(path(file)));
         }