tuned signature;
authorwenzelm
Fri, 02 Jul 2021 12:23:42 +0200
changeset 73921 1f31ed84c467
parent 73920 3b340b44451c
child 73922 3556303bd385
tuned signature;
src/Tools/Setup/isabelle/setup/Build_Scala.java
--- a/src/Tools/Setup/isabelle/setup/Build_Scala.java	Fri Jul 02 12:19:40 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build_Scala.java	Fri Jul 02 12:23:42 2021 +0200
@@ -59,13 +59,13 @@
         public Path path(String file) { return component_dir.resolve(file); }
         public boolean exists(String file) { return Files.exists(path(file)); }
 
-        public String resource_name(String s)
+        public String item_name(String s)
         {
             int i = s.indexOf(':');
             return i > 0 ? s.substring(0, i) : s;
         }
 
-        public String resource_target(String s)
+        public String item_target(String s)
         {
             int i = s.indexOf(':');
             return i > 0 ? s.substring(i + 1) : s;
@@ -104,7 +104,7 @@
             {
                 StringBuilder _shasum = new StringBuilder();
                 for (String s : resources) {
-                    _shasum.append(context.shasum(context.resource_name(s)));
+                    _shasum.append(context.shasum(context.item_name(s)));
                 }
                 for (String s : sources) { _shasum.append(context.shasum(s)); }
                 shasum_sources = _shasum.toString();
@@ -155,8 +155,8 @@
                     /* copy resources */
 
                     for (String s : context.resources()) {
-                        String name = context.resource_name(s);
-                        String target = context.resource_target(s);
+                        String name = context.item_name(s);
+                        String target = context.item_target(s);
                         Path file_name = Path.of(name).normalize().getFileName();
                         Path target_path = Path.of(target).normalize();