package jkind.api.ui.results;

import java.io.IOException;
import java.io.InputStream;

import jkind.api.results.AnalysisResult;
import jkind.api.results.PropertyResult;
import jkind.api.results.ResultsUtil;
import jkind.api.results.Status;
import jkind.api.ui.results.AnalysisResultColumnViewer.Column;
import jkind.results.UnknownProperty;

import org.eclipse.jface.viewers.ColumnLabelProvider;
import org.eclipse.jface.viewers.ColumnViewer;
import org.eclipse.swt.graphics.Image;
import org.eclipse.swt.graphics.ImageData;

public class AnalysisResultLabelProvider extends ColumnLabelProvider {
	private final Column column;

	public AnalysisResultLabelProvider(Column column) {
		this.column = column;
	}

	public AnalysisResultLabelProvider(Column column, ColumnViewer viewer) {
		this.column = column;
		workingSpinner = new Spinner("/icons/working.gif", viewer);
	}

	@Override
	public String getText(Object element) {
		if (element instanceof PropertyResult) {
			PropertyResult pr = (PropertyResult) element;
			switch (column) {
			case PROPERTY:
				return pr.getName();
			case RESULT:
				switch (pr.getStatus()) {
				case WAITING:
					return pr.getStatus().toString();
				case WORKING:
					return pr.getStatus().toString() + "... " + getProgress(pr) + "("
							+ pr.getElapsed() + "s)";
				default:
					return getFinalStatus(pr) + " (" + pr.getElapsed() + "s)";
				}
			}
		} else if (element instanceof AnalysisResult) {
			AnalysisResult result = (AnalysisResult) element;
			switch (column) {
			case PROPERTY:
				return result.getName();
			case RESULT:
				return ResultsUtil.getMultiStatus(result).toString();
			}
		}

		return "";
	}

	private String getProgress(PropertyResult pr) {
		if (pr.getBaseProgress() == 0) {
			return "";
		}

		return trueFor(pr.getBaseProgress()) + " ";
	}

	private String trueFor(int steps) {
		return "[true for " + steps + " steps]";
	}

	private String getFinalStatus(PropertyResult pr) {
		if (pr.getProperty() instanceof UnknownProperty) {
			UnknownProperty up = (UnknownProperty) pr.getProperty();
			return pr.getStatus().toString() + " " + trueFor(up.getTrueFor());
		} else {
			return pr.getStatus().toString();
		}
	}

	private static final Image EMPTY_IMAGE = loadImage("/icons/empty.png");
	private static final Image VALID_IMAGE = loadImage("/icons/valid.png");
	private static final Image INVALID_IMAGE = loadImage("/icons/invalid.png");
	private static final Image UNKNOWN_IMAGE = loadImage("/icons/unknown.png");
	private static final Image WAITING_IMAGE = loadImage("/icons/waiting.png");
	private static final Image CANCEL_IMAGE = loadImage("/icons/cancel.png");
	private static final Image ERROR_IMAGE = loadImage("/icons/error.png");
	private Spinner workingSpinner;

	private static Image loadImage(String filename) {
		try (InputStream stream = AnalysisResultLabelProvider.class.getResourceAsStream(filename)) {
			return new Image(null, new ImageData(stream));
		} catch (IOException e) {
			return null;
		}
	}

	@Override
	public Image getImage(Object element) {
		if (column == Column.PROPERTY) {
			if (element instanceof PropertyResult) {
				PropertyResult pr = (PropertyResult) element;
				return getStatusImage(pr.getStatus());
			} else if (element instanceof AnalysisResult) {
				AnalysisResult result = (AnalysisResult) element;
				return getStatusImage(ResultsUtil.getMultiStatus(result).getOverallStatus());
			}
		}

		return null;
	}

	private Image getStatusImage(Status status) {
		if (status == null) {
			return EMPTY_IMAGE;
		}

		switch (status) {
		case WORKING:
			return workingSpinner.getFrame();
		case VALID:
			return VALID_IMAGE;
		case INVALID:
			return INVALID_IMAGE;
		case UNKNOWN:
			return UNKNOWN_IMAGE;
		case CANCELED:
			return CANCEL_IMAGE;
		case ERROR:
			return ERROR_IMAGE;
		case WAITING:
			return WAITING_IMAGE;
		default:
			return WAITING_IMAGE;
		}
	}

	@Override
	public void dispose() {
		if (workingSpinner != null) {
			workingSpinner.dispose();
		}
	}
}

@@ -310,47 +310,8 @@
 mn;%0D
-%0Aimport jkind.results.UnknownProperty;%0D
 %0A%0D%0Ai
@@ -1242,17 +1242,16 @@
 ) + %22...
- 
 %22 + getP
@@ -1265,16 +1265,17 @@
 (pr) + %22
+ 
 (%22%0D%0A%09%09%09%09
@@ -1798,24 +1798,32 @@
 %09return 
+%22 %5B
 true
-For(
+ for %22 + 
 pr.getBa
@@ -1838,91 +1838,8 @@
 ss()
-) + %22 %22;%0D%0A%09%7D%0D%0A%0D%0A%09private String trueFor(int steps) %7B%0D%0A%09%09return %22%5Btrue for %22 + steps
  + %22
@@ -1924,109 +1924,74 @@
 .get
-Property() instanceof UnknownProperty) %7B%0D%0A%09%09%09UnknownProperty up = (UnknownProperty) pr.getProperty();
+Status() == Status.UNKNOWN %7C%7C pr.getStatus() == Status.CANCELED) %7B
 %0D%0A%09%09
@@ -2030,37 +2030,22 @@
 ) + 
-%22 %22 + trueFor(up.getTrueFor()
+getProgress(pr
 );%0D%0A

Disable progress information on cancelled properties