expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
authorwenzelm
Fri, 09 Jul 2021 21:05:58 +0200
changeset 73957 110a027a5473
parent 73956 ac1884965dc8
child 73958 262dc3bafd15
expand file paths, e.g. to allow $ISABELLE_HOME, $ISABELLE_HOME_USER;
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)));
         }