package acl2s.plugin.certify;
	
	import java.io.File;
	import java.io.IOException;
	import java.io.PrintWriter;
	
	import org.eclipse.core.resources.IFile;
	import org.eclipse.core.resources.ResourcesPlugin;
	import org.eclipse.core.runtime.CoreException;
	import org.eclipse.core.runtime.Path;
	import org.eclipse.jface.resource.ImageDescriptor;
	import org.eclipse.ui.console.IConsoleManager;
	import org.eclipse.ui.console.IOConsoleOutputStream;
	
	import acl2s.lib.certify.CertificationSessionConfig;
	import acl2s.lib.certify.Certifier;
	import acl2s.lib.session.BatchSession;
	import acl2s.plugin.Acl2sPlugin;
	import acl2s.plugin.console.IIdentifiableConsole;
	import acl2s.plugin.console.IKillableConsole;
	import acl2s.plugin.console.MyConsole;
	import acl2s.plugin.misc.Colors;
	import acl2s.plugin.misc.DisplayAsyncRunnable;
	import acl2s.plugin.misc.IOConsoleWriter;
	
	// TODO: abstract away UI dependence and put most in acl2s.lib.certify
	public class CertifyConsole extends MyConsole implements IKillableConsole, IIdentifiableConsole {
		protected final IOConsoleOutputStream stream;
		protected final IOConsoleWriter writer;
		protected final Certifier cert;
		protected final File lispFile;
		protected BatchSession sess = null;
		protected long startTime = 0L;
		
		CertifyConsole(File lispFile) {
			this.lispFile = lispFile;
			this.cert = new Certifier(getConfig(lispFile));
			setName("Certification of " + lispFile.getName());
			setImageDescriptor(image);
			
			stream = newOutputStream();
			stream.setColor(Colors.get(64, 64, 192));
			writer = new IOConsoleWriter(stream);
			
			try {
				getInputStream().close();
			} catch (IOException ioe) {
				// already closed; ok
			}
		}
	
		public Object getIdentity() {
			return lispFile.getAbsolutePath();
		}
	
		public synchronized void kill() {
			if (sess != null) {
				sess.kill();
			}
		}
		
		public synchronized boolean started() {
			return sess != null;
		}
		
		public synchronized boolean finished() {
			return sess != null && !sess.isAlive();
		}
		
		
		public synchronized void start() {

			if (sess != null) throw new IllegalStateException("Already started.");
			
			startTime = System.currentTimeMillis();
			

			sess = cert.createSession();
			notifyAll();
			if (pp != null)	pp.update();
			

			cert.attemptRemoveCertFile();
			
			PrintWriter commentary = new PrintWriter(writer);
			commentary.println("Certification of " + lispFile.getAbsolutePath() + "\n");
	

			if (!cert.buildPreambleCommentary(false, commentary)) {
				return; // failure in extracting preamble
			}
			
			commentary.println("\nStarting ACL2...");
			
			BatchSession.OutputHandler h = sess.createOutputHandler(writer);
			h.appendPostEOFhook(new Runnable() {
				public void run() {
					try {
						if (certFileWritten()) {
							writer.append("\n### CERTIFICATION FILE WRITTEN SUCCESSFULLY ###\n");

						} else if (cert.certFileExists()){
							writer.append("\n!!! CERTIFICATION FILE WRITTEN BUT OUT OF DATE !!!\n");
						} else {
							writer.append("\n!!! CERTIFICATION FILE NOT WRITTEN !!!\n");
						}
					} catch (IOException ioe) {
						handleException(ioe);
					}
				}
			});
			h.appendCloseOnEOFhook();
			h.appendPostEOFhook(new DisplayAsyncRunnable() {
				protected void asyncRun() {
					if (pp != null) {
						pp.update();
					}
					IFile f = ResourcesPlugin.getWorkspace().getRoot().getFileForLocation(new Path(lispFile.getAbsolutePath()));
					if (f != null) {
						try {
							f.getParent().refreshLocal(1, null);
						} catch (CoreException e) {
							Acl2sPlugin.logError("Error refreshing directory following certification", e);
						}
					}
				}
			});
			h.setSnipEnabled(true);
			h.setExceptionHandler(this);
			
			try {
				sess.init();
			} catch (IOException e) {
				commentary.println("Error: " + e.getMessage());
			}
			
			commentary.flush();
			commentary = null; // no more
	
			h.start();
		}
		
		public synchronized void ensureStarted() {
			if (sess == null) {
				start();
			}
		}
		
		public void waitFor() throws InterruptedException {
			BatchSession s;
			synchronized (this) {
				for (;;) {
					s = sess;
					if (s != null) break;
					wait();
				}
			}
			synchronized (s) {
				while (s.isAlive()) {
					s.wait();
				}
			}
		}
		
		public synchronized boolean certFileWritten() {

			if (!finished()) throw new IllegalStateException();

			return cert.certFileNewer();
		}
		
		@Override
		protected void dispose() {
			kill();
			super.dispose();
		}
		
		protected synchronized void doHandleException(IOException e) {
			super.doHandleException(e);
			kill();
			try {
				stream.write(e.getMessage());
			} catch (IOException ioe) {
				// ignore
			}
		}
	
		
		
		
		// STATIC STUFF
		
		public static CertifyConsole findOrCreate(File lispFile) {
			IConsoleManager conman = getConsoleManager();
			synchronized (conman) {
				CertifyConsole cc = find(CertifyConsole.class, lispFile.getAbsolutePath());
				cc = removeIfFinished(cc);
				if (cc != null) {
					return cc;
				}
				// not found or removed finished
				cc = new CertifyConsole(lispFile);
				cc.add();
				cc.show();
				return cc;
			}
		}
		
		static CertificationSessionConfig getConfig(File lispFile) {
			return new CertificationSessionConfig(Acl2sPlugin.getBaseConfig(),lispFile);
		}
	
		static final ImageDescriptor image =
			ImageDescriptor.createFromURL(Acl2sPlugin.getDefault().getBundle().getEntry("/icons/acl2.gif"));
	}