001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.casetool.together.scripts.patternupdate;
012:
013: import java.io.File;
014: import java.io.FileOutputStream;
015: import java.io.InputStream;
016: import java.net.JarURLConnection;
017: import java.util.Enumeration;
018: import java.util.jar.JarEntry;
019: import java.util.jar.JarFile;
020:
021: import com.togethersoft.openapi.ide.IdeContext;
022: import com.togethersoft.openapi.ide.message.IdeMessageManagerAccess;
023: import com.togethersoft.openapi.ide.message.IdeMessageType;
024:
025: import de.uka.ilkd.key.casetool.together.keydebugclassloader.KeyScript;
026:
027: /** The intention of this script is to keep the patterns up to date if another
028: * version of the KeY jar file is used. The patterns cannot
029: * be accessed if they are inside a jar file so we have to copy them to another
030: * place outside the jar file. The position is given by the system property
031: * 'key.pattern.path'. Copying the patterns once after the jar file is installed
032: * raises the problem that after the jar file is updated the changed or new
033: * patterns cannot be used. So we have to check if the installed patterns are up
034: * to date or if new ones have been added and if so to copy them. */
035:
036: public class PatternUpdate extends KeyScript {
037:
038: private JarFile jarFile;
039: private File patternDirectory;
040:
041: /** Reactivate the script */
042: public void run1(IdeContext context) {
043: autorun1();
044: }
045:
046: /**
047: * Activate the script (cmp. KeyScript)
048: */
049: public void autorun1() {
050: IdeMessageManagerAccess.printMessage(
051: IdeMessageType.INFORMATION,
052: "Patternupdate script: started");
053: updatePatterns();
054: IdeMessageManagerAccess.printMessage(
055: IdeMessageType.INFORMATION,
056: "Patternupdate script: finished");
057: }
058:
059: private void updatePatterns() {
060: String patternDirProp = System.getProperty("key.pattern.path");
061: try {
062: if (patternDirProp != null && !"".equals(patternDirProp)) {
063: patternDirectory = new File(patternDirProp);
064: }
065: jarFile = ((JarURLConnection) getClass().getResource(
066: "Manifest.mf").openConnection()).getJarFile();
067: } catch (java.io.IOException io) {
068: System.err.println("Error opening jar file.");
069: io.printStackTrace();
070: return;
071: } catch (ClassCastException cce) {
072: de.uka.ilkd.key.util.Debug.out("No jar file installation.");
073: // no jar file installation
074: return;
075: }
076: copyPatterns();
077: }
078:
079: /** looks through the jar entries and copies the pattern files */
080: private void copyPatterns() {
081: String dest_prefix = patternDirectory.getAbsolutePath() + "/";
082: Enumeration entries = jarFile.entries();
083: while (entries.hasMoreElements()) {
084: JarEntry entry = (JarEntry) entries.nextElement();
085: if (entry.getName().startsWith(
086: "de/uka/ilkd/key/casetool/together/patterns/JAVA/")
087: || entry
088: .getName()
089: .startsWith(
090: "de/uka/ilkd/key/casetool/together/patterns/HelperClasses/")) {
091: if (entry.isDirectory()) {
092: try {
093: createDir(new File(dest_prefix
094: + entry.getName()));
095: } catch (java.io.IOException e) {
096: System.err.println("Cannot create directory "
097: + dest_prefix + entry.getName());
098: e.printStackTrace();
099: }
100: } else {
101: de.uka.ilkd.key.util.Debug
102: .out("Installing new pattern to "
103: + dest_prefix + entry.getName());
104: copyJarEntry(entry, dest_prefix + entry.getName());
105: }
106: }
107: }
108: }
109:
110: /** creates the directory structure of the given file */
111: private void createDir(File dir) throws java.io.IOException {
112: dir.mkdirs();
113: }
114:
115: /** copies the patterns */
116: private void copyJarEntry(JarEntry src, String dest) {
117: try {
118: File destFile = new File(dest);
119: // check if file exists and is equal means same time,
120: // same size
121: if (destFile.lastModified() == src.getTime()
122: && destFile.length() == src.getSize()) {
123: return;
124: }
125: // create directory structure if necessary
126: createDir(destFile.getParentFile());
127: // copy the file
128: InputStream srcStream = jarFile.getInputStream(src);
129: FileOutputStream fos = new FileOutputStream(destFile);
130: int content = srcStream.read();
131: while (content != -1) {
132: fos.write(content);
133: content = srcStream.read();
134: }
135: // mark file to avoid unnecssary copying
136: destFile.setLastModified(src.getTime());
137: fos.close();
138: } catch (java.io.IOException io) {
139: System.err.println("Error writing pattern files.");
140: io.printStackTrace();
141: }
142: }
143:
144: }
|