Support for sorting and disabling proof services

README.txt

@@ -1,6 +1,6 @@
 Protege Proof-Based Explanation
 
-Protege Proof-Based Explanation is Copyright (c) 2014 - 2021 
+Protege Proof-Based Explanation is Copyright (c) 2014 - 2022 
 Live Ontologies Project
 
    Licensed under the Apache License, Version 2.0 (the "License");
@@ -29,7 +29,7 @@ https://github.com/liveontologies/protege-proof-explanation
 
 REQUIREMENTS:
 
-Protege Proof-Based Explanation is tested to work with Protege 5.5.0. It may work 
+Protege Proof-Based Explanation is tested to work with Protege 5.6.0-beta-1-SNAPSHOT. It may work 
 with other versions of Protege.
 
 INSTALLATION:

pom.xml

@@ -89,7 +89,7 @@ is displaying, navigating, and updating those proofs in the user interface.
 
 	<properties>
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
-		<protege.version>5.5.0</protege.version>
+		<protege.version>5.6.0-beta-1-SNAPSHOT</protege.version>
 		<owlapi.version>4.5.7</owlapi.version>
 		<pluginId>${project.groupId}.protege.explanation.proof</pluginId>
 		<extensionId>${pluginId}.service</extensionId>

src/main/java/org/liveontologies/protege/explanation/proof/ProofBasedExplanationResult.java

@@ -34,8 +34,10 @@
 
 import org.liveontologies.protege.explanation.proof.list.ProofFrame;
 import org.liveontologies.protege.explanation.proof.list.ProofFrameList;
+import org.liveontologies.protege.explanation.proof.preferences.ProofBasedExplPrefs;
 import org.liveontologies.protege.explanation.proof.service.ProofService;
 import org.protege.editor.owl.OWLEditorKit;
+import org.protege.editor.owl.ui.explanation.ExplanationPreferences;
 import org.protege.editor.owl.ui.explanation.ExplanationResult;
 import org.semanticweb.owlapi.model.OWLAxiom;
 
@@ -113,15 +115,30 @@ private JComboBox<ProofService> createComboBox(
 				.toArray(new ProofService[proofServices.size()]);
 		final JComboBox<ProofService> selector = new JComboBox<ProofService>(
 				services);
+		final ProofBasedExplPrefs prefs = ProofBasedExplPrefs.create().load();
 		if (services.length > 0) {
-			selector.setSelectedItem(services[0]);
-			proofManager_.selectService(services[0]);
+			ProofService selected = services[0];
+			if (ExplanationPreferences.create().load().useLastExplanationService) {
+				String id = prefs.defaultProofService;
+				if (id != null) {
+					for (ProofService s : proofServices) {
+						if (id.equals(s.getPluginId())) {
+							selected = s;
+						}
+					}
+				}
+			}
+			selector.setSelectedItem(selected);
+			proofManager_.selectService(selected);
 		}
 		selector.addActionListener(new ActionListener() {
 			@Override
 			public void actionPerformed(ActionEvent e) {
-				proofManager_.selectService(
-						(ProofService) selector.getSelectedItem());
+				ProofService selected = (ProofService) selector.getSelectedItem();
+				prefs.load();
+				prefs.defaultProofService = selected.getPluginId();
+				prefs.save();
+				proofManager_.selectService(selected);
 			}
 		});
 		return selector;

src/main/java/org/liveontologies/protege/explanation/proof/ProofBasedExplanationService.java

@@ -56,7 +56,7 @@ public void dispose() {
 
 	@Override
 	public boolean hasExplanation(OWLAxiom axiom) {
-		for (ProofService service : proofServiceMan_.getProofServices()) {
+		for (ProofService service : proofServiceMan_.getEnabledProofServices()) {
 			if (service.hasProof(axiom)) {
 				return true;
 			}

src/main/java/org/liveontologies/protege/explanation/proof/ProofManager.java

@@ -241,7 +241,7 @@ public List<? extends OWLAxiom> getMatchingAxioms(OWLAxiom axiom) {
 	 */
 	public Collection<ProofService> getServices() {
 		List<ProofService> result = new ArrayList<ProofService>();
-		for (ProofService service : proofServiceMan_.getProofServices()) {
+		for (ProofService service : proofServiceMan_.getEnabledProofServices()) {
 			if (service.hasProof(entailment_)) {
 				result.add(service);
 			}

src/main/java/org/liveontologies/protege/explanation/proof/ProofServiceManager.java

@@ -24,7 +24,10 @@
 
 import java.util.ArrayList;
 import java.util.Collection;
+import java.util.Map;
+import java.util.TreeMap;
 
+import org.liveontologies.protege.explanation.proof.preferences.ProofBasedExplPrefs;
 import org.liveontologies.protege.explanation.proof.service.ProofPlugin;
 import org.liveontologies.protege.explanation.proof.service.ProofPluginLoader;
 import org.liveontologies.protege.explanation.proof.service.ProofService;
@@ -45,15 +48,58 @@ public class ProofServiceManager implements Disposable {
 	private final OWLEditorKit kit_;
 
 	private final Collection<ProofService> services_;
+
+	private final Collection<ProofService> enabledServices_;
 
 	private ProofServiceManager(OWLEditorKit kit) throws Exception {
 		this.kit_ = kit;
-		this.services_ = new ArrayList<ProofService>();
+		this.services_ = new ArrayList<>();
+		this.enabledServices_ = new ArrayList<>();
+		reload();
+	}
+
+	public void reload() throws Exception {
 		ProofPluginLoader loader = new ProofPluginLoader(kit_);
+		// use TreeMap for alphabetical ordering
+		Map<String, ProofService> sortedProofServices = new TreeMap<>();
 		for (ProofPlugin plugin : loader.getPlugins()) {
 			ProofService service = plugin.newInstance();
 			service.initialise();
-			services_.add(service);
+			sortedProofServices.put(service.getPluginId(), service);
+		}
+
+		// add ProofServices in the order defined in the preferences
+		final ProofBasedExplPrefs prefs = ProofBasedExplPrefs.create().load();
+		services_.clear();
+		for (String id : prefs.proofServicesList) {
+			ProofService service = sortedProofServices.get(id);
+			if (service != null) {
+				services_.add(service);
+				sortedProofServices.remove(id);
+			}
+		}
+
+		if (!sortedProofServices.isEmpty()) {
+			// add new ProofServices (which do not occur in the preferences yet) in
+			// alphabetical order at the end
+			for (ProofService service: sortedProofServices.values()) {
+				services_.add(service);
+			}
+		}
+
+		// update preferences according to current list (adding new and removing old
+		// ProofServices)
+		prefs.proofServicesList = new ArrayList<>();
+		for (ProofService service : services_) {
+			prefs.proofServicesList.add(service.getPluginId());
+		}
+		prefs.save();
+
+		enabledServices_.clear();
+		for (ProofService service : services_) {
+			if (!prefs.disabledProofServices.contains(service.getPluginId())) {
+				enabledServices_.add(service);
+			}
 		}
 	}
 
@@ -82,5 +128,9 @@ public OWLEditorKit getOWLEditorKit() {
 	public Collection<ProofService> getProofServices() {
 		return services_;
 	}
+
+	public Collection<ProofService> getEnabledProofServices() {
+		return enabledServices_;
+	}
 
 }

src/main/java/org/liveontologies/protege/explanation/proof/preferences/ProofBasedExplPrefs.java

@@ -1,5 +1,8 @@
 package org.liveontologies.protege.explanation.proof.preferences;
 
+import java.util.Collections;
+import java.util.List;
+
 /*-
  * #%L
  * Protege Proof-Based Explanation
@@ -30,7 +33,10 @@ public class ProofBasedExplPrefs {
 	private static final String PREFS_KEY_ = "PROOF_BASED_EXPLANATION_PREFS",
 			RECURSIVE_EXPANSION_LIMIT_KEY_ = "RECURSIVE_EXPANSION_LIMIT",
 			DISPLAYED_INFERENCES_PER_CONCLUSION_LIMIT_KEY = "DISPLAYED_INFERENCES_PER_CONCLUSION_LIMIT",
-			REMOVE_UNNECESSARY_INFERENCES_KEY = "REMOVE_UNNECESSARY_INFERENCES";
+			REMOVE_UNNECESSARY_INFERENCES_KEY = "REMOVE_UNNECESSARY_INFERENCES",
+			DEFAULT_PROOF_SERVICE_ID_KEY_ = "DEFAULT_PROOF_SERVICE",
+			PROOF_SERVICES_LIST_KEY_ = "EXPLANATION_SERVICES_LIST",
+			DISABLED_PROOF_SERVICES_KEY_ = "DISABLED_EXPLANATION_SERVICES";
 
 	public final static String RECURSIVE_EXPANSION_LIMIT_DESCRIPTION = "The maximal number of inferences expanded upon long press or alt + click",
 			DISPLAYED_INFERENCES_PER_CONCLUSION_LIMIT_DESCRIPTION = "The maximal number of inferences displayed at once for each conclusion",
@@ -43,6 +49,12 @@ public class ProofBasedExplPrefs {
 
 	private final static boolean DEFAULT_REMOVE_UNNECESSARY_INFERENCES_ = true;
 
+	private final static String DEFAULT_DEFAULT_PROOF_SERVICE_ID_ = null;
+
+	private final static List<String> DEFAULT_PROOF_SERVICES_LIST_ = Collections.emptyList();
+
+	private final static List<String> DEFAULT_DISABLED_PROOF_SERVICES_ = Collections.emptyList();
+
 	/**
 	 * {@value #RECURSIVE_EXPANSION_LIMIT_DESCRIPTION}
 	 */
@@ -57,6 +69,21 @@ public class ProofBasedExplPrefs {
 	 * {@value #REMOVE_UNNECESSARY_INFERENCES_DESCRIPTION}
 	 */
 	public boolean removeUnnecessaryInferences = DEFAULT_REMOVE_UNNECESSARY_INFERENCES_;
+
+	/**
+	 * The most recently used proof service
+	 */
+	public String defaultProofService = DEFAULT_DEFAULT_PROOF_SERVICE_ID_;
+
+	/**
+	 * User-sorted list of all loaded proof services
+	 */
+	public List<String> proofServicesList =  DEFAULT_PROOF_SERVICES_LIST_;
+
+	/**
+	 * List of all disabled proof services
+	 */
+	public List<String> disabledProofServices = DEFAULT_DISABLED_PROOF_SERVICES_;
 
 	private ProofBasedExplPrefs() {
 
@@ -85,6 +112,15 @@ public ProofBasedExplPrefs load() {
 		removeUnnecessaryInferences = prefs.getBoolean(
 				REMOVE_UNNECESSARY_INFERENCES_KEY,
 				DEFAULT_REMOVE_UNNECESSARY_INFERENCES_);
+		defaultProofService = prefs.getString(
+				DEFAULT_PROOF_SERVICE_ID_KEY_,
+				DEFAULT_DEFAULT_PROOF_SERVICE_ID_);
+		proofServicesList = prefs.getStringList(
+				PROOF_SERVICES_LIST_KEY_,
+				DEFAULT_PROOF_SERVICES_LIST_);
+		disabledProofServices = prefs.getStringList(
+				DISABLED_PROOF_SERVICES_KEY_,
+				DEFAULT_DISABLED_PROOF_SERVICES_);
 		return this;
 	}
 
@@ -95,13 +131,19 @@ public ProofBasedExplPrefs save() {
 				displayedInferencesPerConclusionLimit);
 		prefs.putBoolean(REMOVE_UNNECESSARY_INFERENCES_KEY,
 				removeUnnecessaryInferences);
+		prefs.putString(DEFAULT_PROOF_SERVICE_ID_KEY_, defaultProofService);
+		prefs.putStringList(PROOF_SERVICES_LIST_KEY_, proofServicesList);
+		prefs.putStringList(DISABLED_PROOF_SERVICES_KEY_, disabledProofServices);
 		return this;
 	}
 
 	public ProofBasedExplPrefs reset() {
 		recursiveExpansionLimit = DEFAULT_RECURSIVE_EXPANSION_LIMIT_;
 		displayedInferencesPerConclusionLimit = DEFAULT_DISPLAYED_INFERENCES_PER_CONCLUSION_LIMIT_;
 		removeUnnecessaryInferences = DEFAULT_REMOVE_UNNECESSARY_INFERENCES_;
+		defaultProofService = DEFAULT_DEFAULT_PROOF_SERVICE_ID_;
+		proofServicesList = DEFAULT_PROOF_SERVICES_LIST_;
+		disabledProofServices = DEFAULT_DISABLED_PROOF_SERVICES_;
 		return this;
 	}