Update the GATE development environment configuration data in the user's gate.xml file (create one if it doesn't exist).
()
| 844 | * <TT>gate.xml</TT> file (create one if it doesn't exist). |
| 845 | */ |
| 846 | public static void writeUserConfig() throws GateException { |
| 847 | |
| 848 | //if we are running in a sandbox then don't try and write anything |
| 849 | if (sandboxed) return; |
| 850 | |
| 851 | String pluginsHomeStr = null; |
| 852 | if(pluginsHome != null) { |
| 853 | try { |
| 854 | pluginsHomeStr = pluginsHome.getCanonicalPath(); |
| 855 | } catch(IOException ioe) { |
| 856 | throw new GateRuntimeException( |
| 857 | "Problem while locating the plug-ins home!", ioe); |
| 858 | } |
| 859 | } |
| 860 | |
| 861 | // update the values for knownPluginPath |
| 862 | String knownPluginPath = ""; |
| 863 | Set<Plugin> defaultPlugins = PluginUpdateManager.getDefaultPlugins(); |
| 864 | Iterator<Plugin> pluginIter = getKnownPlugins().iterator(); |
| 865 | while(pluginIter.hasNext()) { |
| 866 | Plugin aPlugin = pluginIter.next(); |
| 867 | String pluginStr = null; |
| 868 | if(aPlugin instanceof Plugin.Maven) { |
| 869 | Plugin.Maven mavenPlugin = (Plugin.Maven)aPlugin; |
| 870 | if(!defaultPlugins.contains(aPlugin)) { |
| 871 | pluginStr = "[" + mavenPlugin.getGroup() + ":" |
| 872 | + mavenPlugin.getArtifact() + ":" + mavenPlugin.getVersion() + "]"; |
| 873 | } |
| 874 | } else if(aPlugin instanceof Plugin.Directory) { |
| 875 | URL aPluginURL = aPlugin.getBaseURL(); |
| 876 | // do not save installed plug-ins - they get loaded automatically |
| 877 | if(aPluginURL.getProtocol().equals("file")) { |
| 878 | File pluginDirectory = Files.fileFromURL(aPluginURL); |
| 879 | try { |
| 880 | if(pluginsHomeStr != null && pluginDirectory.getCanonicalPath().startsWith(pluginsHomeStr)) |
| 881 | continue; |
| 882 | } catch(IOException ioe) { |
| 883 | throw new GateRuntimeException("Problem while locating the plug-in" |
| 884 | + aPluginURL.toString(), ioe); |
| 885 | } |
| 886 | } |
| 887 | pluginStr = aPluginURL.toExternalForm(); |
| 888 | } // no else - we don't save other types of plugin |
| 889 | if(pluginStr != null) { |
| 890 | if(knownPluginPath.length() > 0) knownPluginPath += ";"; |
| 891 | knownPluginPath += pluginStr; |
| 892 | } |
| 893 | } |
| 894 | getUserConfig().put(KNOWN_PLUGIN_PATH_KEY, knownPluginPath); |
| 895 | |
| 896 | // update the autoload plugin list |
| 897 | String loadPluginPath = ""; |
| 898 | pluginIter = getAutoloadPlugins().iterator(); |
| 899 | while(pluginIter.hasNext()) { |
| 900 | Plugin aPlugin = pluginIter.next(); |
| 901 | String pluginStr = null; |
| 902 | if(aPlugin instanceof Plugin.Maven) { |
| 903 | Plugin.Maven mavenPlugin = (Plugin.Maven)aPlugin; |