001: package de.uka.ilkd.key.casetool.eclipse;
002:
003: /*
004: * This file is part of KeY - Integrated Deductive Software Design
005: * Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
006: * Universitaet Koblenz-Landau, Germany
007: * Chalmers University of Technology, Sweden
008: *
009: * The KeY system is protected by the GNU General Public License.
010: */
011:
012: import java.io.File;
013: import java.util.LinkedList;
014: import java.util.MissingResourceException;
015: import java.util.ResourceBundle;
016:
017: import org.eclipse.core.resources.IProject;
018: import org.eclipse.core.resources.IResourceChangeEvent;
019: import org.eclipse.core.resources.IResourceChangeListener;
020: import org.eclipse.core.resources.IResourceDelta;
021: import org.eclipse.core.resources.IResourceDeltaVisitor;
022: import org.eclipse.core.resources.ResourcesPlugin;
023: import org.eclipse.core.runtime.CoreException;
024: import org.eclipse.jface.dialogs.MessageDialog;
025: import org.eclipse.ui.PlatformUI;
026: import org.eclipse.ui.plugin.AbstractUIPlugin;
027: import org.osgi.framework.BundleContext;
028:
029: import de.uka.ilkd.key.gui.Main;
030: import de.uka.ilkd.key.proof.init.JavaInput;
031: import de.uka.ilkd.key.proof.init.JavaInputWithJMLSpecBrowser;
032: import de.uka.ilkd.key.proof.init.ProblemInitializer;
033: import de.uka.ilkd.key.proof.init.ProofInputException;
034:
035: /**
036: * @author Marius Hillenbrand
037: *
038: * The main plugin class to be used in the desktop.
039: *
040: * The PlugIn instance is a singleton in Eclipse, thereby use getDefault() for
041: * access
042: */
043: /**
044: * @author hillen
045: *
046: */
047: public class KeYPlugin extends AbstractUIPlugin implements
048: IResourceChangeListener {
049:
050: /**
051: * Nested class to analyze resource change deltas.
052: * If resources in a project whose source code we loaded into KeY are changed,
053: * remove it from the list of loaded projects.
054: */
055: private final class ProjectChangeDeltaInspector implements
056: IResourceDeltaVisitor {
057:
058: /* (non-Javadoc)
059: * @see org.eclipse.core.resources.IResourceDeltaVisitor#visit(org.eclipse.core.resources.IResourceDelta)
060: */
061: public boolean visit(IResourceDelta delta) throws CoreException {
062:
063: IProject containingProject = delta.getResource()
064: .getProject();
065: // if a proof has been started in this project and the sourcecode has been marked as loaded
066: // remove this now to trigger a reload when a new proof is to be started
067: if (loadedProjects.contains(containingProject)) {
068: loadedProjects.remove(containingProject);
069: }
070:
071: if (loadedProjects.size() == 0)
072: return false;
073: else
074: return true;
075:
076: }
077: }
078:
079: protected static final int PROJECT_ALREADY_OPEN = 1;
080:
081: protected static final int PROJECT_LOAD_SUCESSFUL = 2;
082:
083: protected static final int PROJECT_LOAD_CANCELED = 3;
084:
085: protected static final int PROJECT_LOAD_FAILED = 4;
086:
087: // The shared instance.
088: private static KeYPlugin plugin;
089:
090: // Resource bundle.
091: private ResourceBundle resourceBundle;
092:
093: /**
094: * a list of the javaProjects which currently have a model loaded into the
095: * KeY prover
096: */
097: private LinkedList loadedProjects = new LinkedList();
098:
099: /**
100: * have we registered as resource change listener yet ?
101: */
102: private boolean registeredAsResourceChangeListener = false;
103:
104: /**
105: * The constructor.
106: */
107: public KeYPlugin() {
108: super ();
109: plugin = this ;
110: }
111:
112: /**
113: * This method is called upon plug-in activation
114: */
115: public void start(BundleContext context) throws Exception {
116: super .start(context);
117: Main.standalone = false;
118: }
119:
120: /**
121: * This method is called when the plug-in is stopped
122: */
123: public void stop(BundleContext context) throws Exception {
124: super .stop(context);
125: plugin = null;
126: resourceBundle = null;
127: }
128:
129: /**
130: * Returns the shared instance.
131: */
132: public static KeYPlugin getDefault() {
133: return plugin;
134: }
135:
136: /**
137: * Returns the string from the plugin's resource bundle, or 'key' if not
138: * found.
139: */
140: public static String getResourceString(String key) {
141: ResourceBundle bundle = KeYPlugin.getDefault()
142: .getResourceBundle();
143: try {
144: return (bundle != null) ? bundle.getString(key) : key;
145: } catch (MissingResourceException e) {
146: return key;
147: }
148: }
149:
150: /**
151: * Returns the plugin's resource bundle,
152: */
153: public ResourceBundle getResourceBundle() {
154: try {
155: if (resourceBundle == null)
156: resourceBundle = ResourceBundle
157: .getBundle("de.uka.ilkd.key.casetool.eclipse.KeYPluginResources");
158: } catch (MissingResourceException x) {
159: resourceBundle = null;
160: }
161: return resourceBundle;
162: }
163:
164: /**
165: * @param project
166: * @return
167: */
168: protected int assertProjectParsed(IProject project) {
169: return assertProjectParsed(project, false);
170: }
171:
172: /**
173: * if necessary loads the current project into the KeY prover. Is
174: * synchronized to protect LinkedList loadedProjects against simultaneous
175: * manipulation by the resource change listeners
176: *
177: * TODO: recursively parse source fragments linked from anywhere else -
178: * sensefully integrateable in KeY ??
179: *
180: * @param project
181: * the eclipse project which should be loaded
182: * @param jmlBrowserIntended
183: * is it intended to open the JML browser or would this be a
184: * side-effect?
185: * @return status whether the project was already opened before or the load
186: * was successful / failed
187: *
188: */
189: protected synchronized int assertProjectParsed(IProject project,
190: boolean jmlBrowserIntended) {
191:
192: if (!loadedProjects.contains(project)) {
193:
194: // project's java model has not been loaded into KeY yet, do this
195: // now
196:
197: String inputName = "eclipse-project_" + project.getName();
198: File location = project.getLocation().toFile();
199:
200: Main main = Main.getInstance(false);
201:
202: JavaInput input;
203:
204: if (jmlBrowserIntended) {
205:
206: input = new JavaInputWithJMLSpecBrowser(inputName,
207: location, false, main.getProgressMonitor());
208:
209: } else {
210: input = new JavaInput(inputName, location, main
211: .getProgressMonitor());
212: }
213:
214: ProblemInitializer problemInit = new ProblemInitializer(
215: main);
216:
217: String error = "Prover init for " + location + " failed.";
218: try {
219: problemInit.startProver(input, input);
220: error = "";
221: } catch (ProofInputException pie) {
222: error = pie.getMessage();
223: }
224:
225: if (error.length() == 0) {
226:
227: loadedProjects.add(project);
228:
229: // now register as resource change listener, if not done before
230: if (!registeredAsResourceChangeListener) {
231: ResourcesPlugin.getWorkspace()
232: .addResourceChangeListener(this ,
233: IResourceChangeEvent.POST_CHANGE);
234: registeredAsResourceChangeListener = true;
235: }
236: return PROJECT_LOAD_SUCESSFUL;
237:
238: } else {
239:
240: MessageDialog.openError(PlatformUI.getWorkbench()
241: .getActiveWorkbenchWindow().getShell(),
242: "Error loading java model into KeY prover",
243: "While loading this project, the following error"
244: + " occured:\n" + error);
245: return PROJECT_LOAD_FAILED;
246: }
247:
248: } else {
249: return PROJECT_ALREADY_OPEN;
250: }
251: }
252:
253: /**
254: * Just opens the JML Specification browser in the KeY prover which knows
255: * about the java models loaded before. This may only be called *after*
256: * assertProjectParsed(), otherwise the JML Spec Bowser will only show the
257: * built-in specs.
258: */
259: public void openJMLSpecBrowserOnCurrentLoadedModel() {
260:
261: Main key = Main.getInstance(true);
262: Main.setStandalone(false);
263: key.toFront();
264: key.showSpecBrowser();
265:
266: }
267:
268: /* (non-Javadoc)
269: * @see org.eclipse.core.resources.IResourceChangeListener#resourceChanged(org.eclipse.core.resources.IResourceChangeEvent)
270: */
271: public synchronized void resourceChanged(IResourceChangeEvent event) {
272:
273: if (!(loadedProjects.size() == 0)) { // do nothing when we don't observe any projects
274: try {
275: event.getDelta().accept(
276: new ProjectChangeDeltaInspector());
277: } catch (CoreException e) {
278: // TODO Auto-generated catch block
279: e.printStackTrace();
280: }
281: }
282:
283: }
284:
285: /**
286: * starts the KeY Prover in standalone mode (i.e. no Project selection required)
287: */
288: public void openKeY() {
289: Main.getInstance(true).toFront();
290: Main.setStandalone(false);
291: }
292: }
|