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 }