diff --git a/Makefile b/Makefile index 32781edb28435a71a3b36e805240d2ed5cbd3e2b..a910f5c330eb7dd133595c17f356a00ac3b708d2 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 8f038b5364cadf60cb58dfe244cc8c1b1d97f492..86a89775f68a7f2584156cb2cba6b3a35f938092 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 9148f0bdad6d89cf387bb7123c8a9befeb16e916..20854775d716b4659953628a3ac5191569cb6a65 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) {