mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-09-27 10:03:11 +07:00
workaround for GwtLanguageLevel pusher to affect java language level
This commit is contained in:
+10
-1
@@ -107,7 +107,16 @@ public class JavaLanguageLevelPusher implements FilePropertyPusher<LanguageLevel
|
||||
DataInputOutputUtil.writeINT(oStream, level.ordinal());
|
||||
oStream.close();
|
||||
|
||||
PushedFilePropertiesUpdater.getInstance(project).filePropertiesChanged(fileOrDir, f -> isJavaLike(f.getFileType()));
|
||||
// Todo: GwtLanguageLevelPusher changes java language level for single files without firing filePropertiesChanged
|
||||
// so code below doesn't work.
|
||||
// Uncomment it and remove older code once the problem is fixed
|
||||
//PushedFilePropertiesUpdater.getInstance(project).filePropertiesChanged(fileOrDir, f -> isJavaLike(f.getFileType()));
|
||||
|
||||
for (VirtualFile child : fileOrDir.getChildren()) {
|
||||
if (!child.isDirectory() && isJavaLike(child.getFileType())) {
|
||||
PushedFilePropertiesUpdater.getInstance(project).filePropertiesChanged(child);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
private static boolean isJavaLike(FileType type) {
|
||||
|
||||
Reference in New Issue
Block a user