From 0f3ce5e298ee9d2bd3c88f2f51a696445ba1ffaf Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Mon, 23 Sep 2019 17:43:37 +0200
Subject: [PATCH] improve operations popup menu for large nr of events
custom guard and parameter dialog entries at top
for large number of events
---
.../prob/ui/operationview/ParameterMenu.java | 24 +++++++++++++++----
1 file changed, 19 insertions(+), 5 deletions(-)
diff --git a/de.prob.ui/src/de/prob/ui/operationview/ParameterMenu.java b/de.prob.ui/src/de/prob/ui/operationview/ParameterMenu.java
index 7405a6bd..5b19cc4d 100644
--- a/de.prob.ui/src/de/prob/ui/operationview/ParameterMenu.java
+++ b/de.prob.ui/src/de/prob/ui/operationview/ParameterMenu.java
@@ -31,11 +31,14 @@ public class ParameterMenu extends ExtensionContributionFactory {
nondetcounter = 0;
- for (Operation operation : operations) {
- long id = operation.getId();
- additions.addContributionItem(
- createEntry(serviceLocator, operation, id), null);
-
+ if (operations.size()<=10) {
+ // if number of operations small: show enabled operations first
+ for (Operation operation : operations) {
+ long id = operation.getId();
+ additions.addContributionItem(
+ createEntry(serviceLocator, operation, id), null);
+
+ }
}
CommandContributionItemParameter contributionParameters = new CommandContributionItemParameter(
@@ -54,6 +57,17 @@ public class ParameterMenu extends ExtensionContributionFactory {
contributionCustomGuard);
additions.addContributionItem(customGuardDialogItem, null);
+ if (operations.size()>10) {
+ // if number of operations large: show enabled operations last
+ // TODO: nested view according to parameters or group entries together into submenus of 20 operations or so
+ for (Operation operation : operations) {
+ long id = operation.getId();
+ additions.addContributionItem(
+ createEntry(serviceLocator, operation, id), null);
+
+ }
+ }
+
}
private CommandContributionItem createEntry(
--
GitLab