# HG changeset patch
# User wenzelm
# Date 1625221422 -7200
# Node ID 1f31ed84c46798fc37cd784c462c5a32e527c972
# Parent  3b340b44451cd214e3ddc184bad8cb5f564c694f
tuned signature;

diff -r 3b340b44451c -r 1f31ed84c467 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();