001 package org.meta_environment.eclipse.editors;
002
003 import java.io.ByteArrayInputStream;
004
005 import org.eclipse.core.resources.IFile;
006 import org.eclipse.core.resources.IResource;
007 import org.eclipse.core.resources.ResourcesPlugin;
008 import org.eclipse.core.runtime.CoreException;
009 import org.eclipse.core.runtime.NullProgressMonitor;
010 import org.eclipse.core.runtime.Path;
011 import org.eclipse.imp.editor.UniversalEditor;
012 import org.eclipse.ui.IWorkbench;
013 import org.eclipse.ui.IWorkbenchPage;
014 import org.eclipse.ui.IWorkbenchWindow;
015 import org.eclipse.ui.PartInitException;
016 import org.eclipse.ui.PlatformUI;
017 import org.eclipse.ui.part.FileEditorInput;
018 import org.meta_environment.eclipse.Activator;
019
020 import toolbus.adapter.eclipse.EclipseTool;
021
022 public class EditorTool extends EclipseTool {
023 private static class InstanceKeeper {
024 private static EditorTool sInstance = new EditorTool();
025 static {
026 sInstance.connect();
027 }
028 }
029
030 public static EditorTool getInstance() {
031 return InstanceKeeper.sInstance;
032 }
033
034 private EditorTool() {
035 super("editor-tool");
036 }
037
038 public void open(final String filename, String language) {
039 System.err.println("ET: file: " + filename + " language: " + language);
040
041 PlatformUI.getWorkbench().getDisplay().asyncExec(new Runnable() {
042 public void run() {
043 IWorkbench wb = PlatformUI.getWorkbench();
044 IWorkbenchWindow win = wb.getActiveWorkbenchWindow();
045
046 if (win != null) {
047 IWorkbenchPage page = win.getActivePage();
048
049 if (page != null) {
050 IFile file = ResourcesPlugin.getWorkspace().getRoot()
051 .getFileForLocation(new Path(filename));
052
053 try {
054 if (!file.exists()) {
055 file.create(new ByteArrayInputStream(
056 new byte[0]), true,
057 new NullProgressMonitor());
058 }
059 page.openEditor(new FileEditorInput(file),
060 UniversalEditor.EDITOR_ID);
061 } catch (PartInitException e) {
062 Activator.getInstance()
063 .logException(
064 "Could not open editor for: "
065 + filename, e);
066 } catch (CoreException e) {
067 Activator.getInstance()
068 .logException(
069 "Could not open editor for: "
070 + filename, e);
071 }
072 }
073 }
074 }
075 });
076 }
077
078 public void editTerm(final String filename, String language, String content) {
079 System.err.println("ET: file: " + filename + " language: " + language + " content: " + content);
080
081 IFile file = ResourcesPlugin.getWorkspace().getRoot().getFileForLocation(new Path(filename));
082
083 try {
084 if(!file.exists()){
085 file.create(new ByteArrayInputStream(new byte[0]), true, new NullProgressMonitor());
086 }
087
088 file.setContents(new ByteArrayInputStream(content.toString().getBytes()), IResource.FORCE, new NullProgressMonitor());
089 } catch (CoreException e) {
090 Activator.getInstance().logException("Could not open editor for: " + filename, e);
091 }
092
093 open(filename, language);
094 }
095 }