From 5c8a7e7545255f27cf9f90c23a47db4d1b1ea346 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Mon, 15 Jun 2020 14:05:19 +0200
Subject: [PATCH] Update on TTool action: select panel by name
---
Makefile | 2 +-
src/main/java/cli/Action.java | 34 ++++++++++++++++++++++++++++++++++
src/main/java/ui/MainGUI.java | 13 +++++++++++++
3 files changed, 48 insertions(+), 1 deletion(-)
diff --git a/Makefile b/Makefile
index 32781edb28..a910f5c330 100755
--- a/Makefile
+++ b/Makefile
@@ -71,7 +71,7 @@ Please report bugs or suggestions of improvements to:
endef
export HELP_message
-.PHONY: ttool clean launcher graphminimize graphshow tiftranslator tmltranslator rundse remotesimulator webcrawler documentation help ultraclean publish_jar preinstall test git
+.PHONY: ttool clean launcher graphminimize graphshow ttool-cli tiftranslator tmltranslator rundse remotesimulator webcrawler documentation help ultraclean publish_jar preinstall test git
help:
@echo "$$HELP_message"
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index 8f038b5364..86a89775f6 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -97,6 +97,8 @@ public class Action extends Command {
private final static String NAVIGATE_PANEL_TO_LEFT = "navigate-panel-to-left";
private final static String NAVIGATE_PANEL_TO_RIGHT = "navigate-panel-to-right";
+ private final static String SELECT_PANEL = "select-panel";
+
private final static String NAVIGATE_LEFT_PANEL = "navigate-left-panel";
private final static String AVATAR_RG_GENERATION = "avatar-rg";
@@ -699,6 +701,35 @@ public class Action extends Command {
}
};
+ Command selectPanel = new Command() {
+ public String getCommand() {
+ return SELECT_PANEL;
+ }
+
+ public String getShortCommand() {
+ return "sp";
+ }
+
+ public String getDescription() {
+ return "Select the edition panel with a name";
+ }
+
+ public String executeCommand(String command, Interpreter interpreter) {
+ if (!interpreter.isTToolStarted()) {
+ return Interpreter.TTOOL_NOT_STARTED;
+ }
+
+ String[] commands = command.split(" ");
+ if (commands.length < 1) {
+ return Interpreter.BAD;
+ }
+
+ interpreter.mgui.selectPanelByName(commands[0]);
+
+ return null;
+ }
+ };
+
Command movePanelToTheLeftPanel = new Command() {
public String getCommand() {
@@ -742,6 +773,8 @@ public class Action extends Command {
return Interpreter.TTOOL_NOT_STARTED;
}
+
+
interpreter.mgui.requestMoveRightTab(interpreter.mgui.getCurrentJTabbedPane().getSelectedIndex());
return null;
@@ -1096,6 +1129,7 @@ public class Action extends Command {
addAndSortSubcommand(diplodocusRemoveNoC);
addAndSortSubcommand(movePanelToTheLeftPanel);
addAndSortSubcommand(movePanelToTheRightPanel);
+ addAndSortSubcommand(selectPanel);
addAndSortSubcommand(compareUppaal);
addAndSortSubcommand(generic);
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index 9148f0bdad..20854775d7 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -8224,6 +8224,19 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
changeMade(null, -1);
}
+
+ public boolean selectPanelByName(String name) {
+ for (int i = 0; i < mainTabbedPane.getTabCount(); i++) {
+ if (mainTabbedPane.getTitleAt(i).equals(name)) {
+ mainTabbedPane.setSelectedIndex(i);
+ return true;
+ }
+
+ }
+ return false;
+ }
+
+
public void requestMoveRightTab(int index) {
// TraceManager.addDev("Move right");
if (index > tabs.size() - 2) {
--
GitLab