package org.liveontologies.protege.justification.proof;

import java.util.Set;

import org.liveontologies.protege.explanation.justification.service.JustificationComputation;
import org.liveontologies.protege.explanation.justification.service.JustificationListener;
import org.liveontologies.protege.justification.proof.service.JustificationCompleteProof;
import org.liveontologies.puli.justifications.InterruptMonitor;
import org.liveontologies.puli.justifications.MinimalSubsetEnumerator;
import org.liveontologies.puli.justifications.MinimalSubsetEnumerators;
import org.semanticweb.owlapi.model.OWLAxiom;

public class ProofJustificationComputation extends JustificationComputation
		implements InterruptMonitor,
		MinimalSubsetEnumerator.Listener<OWLAxiom> {

	private final JustificationProofManager manager_;

	public ProofJustificationComputation(JustificationProofManager manager,
			JustificationListener listener,
			JustificationComputation.InterruptMonitor monitor) {
		super(listener, monitor);
		this.manager_ = manager;
	}

	@Override
	public void startComputation() {
		enumerateJustifications(manager_.getProof());
	}

	public <C> void enumerateJustifications(
			JustificationCompleteProof<C> proof) {
		MinimalSubsetEnumerators.enumerateJustifications(proof.getGoal(), proof,
				proof, this, this);
	}

	@Override
	public void newMinimalSubset(Set<OWLAxiom> set) {
		notifyJustificationFound(set);
	}

}

@@ -258,16 +258,117 @@
 stener;%0A
+import org.liveontologies.protege.explanation.justification.service.JustificationPriorityComparator;%0A
 import o
@@ -656,16 +656,82 @@
 rators;%0A
+import org.liveontologies.puli.justifications.PriorityComparator;%0A
 import o
@@ -976,16 +976,84 @@
 ager_;%0A%0A
+%09private PriorityComparator%3CSet%3COWLAxiom%3E, ?%3E priorityCompatator_;%0A%0A
 %09public 
@@ -1263,24 +1263,446 @@
 anager;%0A%09%7D%0A%0A
+%09@Override%0A%09public %3CP%3E boolean setPrefferredPriority(%0A%09%09%09JustificationPriorityComparator%3CP%3E comparator) %7B%0A%09%09this.priorityCompatator_ = new PriorityComparator%3CSet%3COWLAxiom%3E, P%3E() %7B%0A%0A%09%09%09@Override%0A%09%09%09public int compare(P p1, P p2) %7B%0A%09%09%09%09return comparator.compare(p1, p2);%0A%09%09%09%7D%0A%0A%09%09%09@Override%0A%09%09%09public P getPriority(Set%3COWLAxiom%3E justification) %7B%0A%09%09%09%09return comparator.getPriority(justification);%0A%09%09%09%7D%0A%09%09%7D;%0A%09%09return true;%0A%09%7D%0A%0A
 %09@Override%0A%09
@@ -1870,16 +1870,54 @@
 roof) %7B%0A
+%09%09if (priorityCompatator_ == null) %7B%0A%09
 %09%09Minima
@@ -1979,25 +1979,159 @@
 l(),
- proof,%0A%09%09%09%09proof
+%0A%09%09%09%09%09proof, proof, this, this);%0A%09%09%7D else %7B%0A%09%09%09MinimalSubsetEnumerators.enumerateJustifications(proof.getGoal(),%0A%09%09%09%09%09proof, proof, priorityCompatator_
 , th
@@ -2141,16 +2141,20 @@
  this);%0A
+%09%09%7D%0A
 %09%7D%0A%0A%09@Ov

Use the preferred justification priority