equal
deleted
inserted
replaced
109 // Calculate the name of the Java source file to be generated. |
109 // Calculate the name of the Java source file to be generated. |
110 int dp = src.getName().lastIndexOf("."); |
110 int dp = src.getName().lastIndexOf("."); |
111 String classname = src.getName().substring(0,dp); |
111 String classname = src.getName().substring(0,dp); |
112 |
112 |
113 // Sort the properties in increasing key order. |
113 // Sort the properties in increasing key order. |
114 List<String> sortedKeys = new ArrayList<String>(); |
114 List<String> sortedKeys = new ArrayList<>(); |
115 for (Object key : p.keySet()) { |
115 for (Object key : p.keySet()) { |
116 sortedKeys.add((String)key); |
116 sortedKeys.add((String)key); |
117 } |
117 } |
118 Collections.sort(sortedKeys); |
118 Collections.sort(sortedKeys); |
119 Iterator<String> keys = sortedKeys.iterator(); |
119 Iterator<String> keys = sortedKeys.iterator(); |
138 } |
138 } |
139 } |
139 } |
140 |
140 |
141 Set<URI> as = packageArtifacts.get(pkgName); |
141 Set<URI> as = packageArtifacts.get(pkgName); |
142 if (as == null) { |
142 if (as == null) { |
143 as = new HashSet<URI>(); |
143 as = new HashSet<>(); |
144 packageArtifacts.put(pkgName, as); |
144 packageArtifacts.put(pkgName, as); |
145 } |
145 } |
146 as.add(dest.toURI()); |
146 as.add(dest.toURI()); |
147 |
147 |
148 if (dest.exists() && dest.lastModified() > src.lastModified()) { |
148 if (dest.exists() && dest.lastModified() > src.lastModified()) { |